MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitr3ri Structured version   Visualization version   GIF version

Theorem 3bitr3ri 289
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 21-Jun-1993.)
Hypotheses
Ref Expression
3bitr3i.1 (𝜑𝜓)
3bitr3i.2 (𝜑𝜒)
3bitr3i.3 (𝜓𝜃)
Assertion
Ref Expression
3bitr3ri (𝜃𝜒)

Proof of Theorem 3bitr3ri
StepHypRef Expression
1 3bitr3i.3 . 2 (𝜓𝜃)
2 3bitr3i.1 . . 3 (𝜑𝜓)
3 3bitr3i.2 . . 3 (𝜑𝜒)
42, 3bitr3i 264 . 2 (𝜓𝜒)
51, 4bitr3i 264 1 (𝜃𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 194
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 195
This theorem is referenced by:  bigolden  971  2eu8  2547  2ralor  3087  sbcco  3424  symdifass  3814  dfiin2g  4483  zfpair  4826  dffun6f  5804  fsplit  7146  axdc3lem4  9135  istrkg2ld  25076  legso  25212  disjunsn  28595  gtiso  28667  fpwrelmapffslem  28701  qqhre  29198  dfpo2  30704  dfdm5  30727  dfrn5  30728  nofulllem5  30911  brimg  31020  dfrecs2  31033  poimirlem25  32400  cdlemefrs29bpre0  34498  cdlemftr3  34667  dffrege115  37088  brco3f1o  37147  elnev  37457  2reu8  39638
  Copyright terms: Public domain W3C validator