Home brismu bridi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  qi1i

Theorem qi1i 235
Description: Inference form of ax-qi1 234 (Contributed by la korvo, 23-Jun-2024.)
Hypothesis
Ref Expression
qi1i.0ro da zo'u ganai broda gi brode
Assertion
Ref Expression
qi1iganai ro da zo'u broda gi ro da zo'u brode

Proof of Theorem qi1i
StepHypRef Expression
1 qi1i.0 . 2ro da zo'u ganai broda gi brode
2 ax-qi1 234 . 2ganai ro da zo'u ganai broda gi brode gi ganai ro da zo'u broda gi ro da zo'u brode
31, 2ax-mp 10 1ganai ro da zo'u broda gi ro da zo'u brode
Colors of variables: sumti selbri bridi
Syntax hints:   ganai bgan 9   ro brd 222
This theorem was proved from axioms:  ax-mp 10  ax-qi1 234
This theorem is referenced by:  qi1-mp  236
  Copyright terms: Public domain W3C validator