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

Theorem 3bitr3ri 291
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 266 . 2 (𝜓𝜒)
51, 4bitr3i 266 1 (𝜃𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 196
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 197
This theorem is referenced by:  bigolden  976  2eu8  2559  2ralor  3107  sbcco  3456  symdifass  3851  dfiin2g  4551  zfpair  4902  dffun6f  5900  fsplit  7279  axdc3lem4  9272  istrkg2ld  25353  legso  25488  disjunsn  29391  gtiso  29463  fpwrelmapffslem  29492  qqhre  30049  dfpo2  31631  dfdm5  31660  dfrn5  31661  brimg  32028  dfrecs2  32041  poimirlem25  33414  cdlemefrs29bpre0  35510  cdlemftr3  35679  dffrege115  38098  brco3f1o  38157  elnev  38465  2reu8  40961
  Copyright terms: Public domain W3C validator