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  1014  2eu8  2698  2ralor  3247  sbcco  3599  symdifass  3996  dfiin2g  4705  zfpair  5053  dffun6f  6063  fsplit  7451  axdc3lem4  9487  istrkg2ld  25579  legso  25714  disjunsn  29735  gtiso  29808  fpwrelmapffslem  29837  qqhre  30394  dfpo2  31973  dfdm5  32002  dfrn5  32003  brimg  32371  dfrecs2  32384  poimirlem25  33765  cdlemefrs29bpre0  36204  cdlemftr3  36373  dffrege115  38792  brco3f1o  38851  elnev  39159  2reu8  41716
  Copyright terms: Public domain W3C validator