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  1012  2eu8  2709  2ralor  3257  sbcco  3610  symdifass  4002  dfiin2g  4687  zfpair  5032  dffun6f  6045  fsplit  7433  axdc3lem4  9477  istrkg2ld  25580  legso  25715  disjunsn  29745  gtiso  29818  fpwrelmapffslem  29847  qqhre  30404  dfpo2  31983  dfdm5  32012  dfrn5  32013  brimg  32381  dfrecs2  32394  poimirlem25  33767  cdlemefrs29bpre0  36205  cdlemftr3  36374  dffrege115  38798  brco3f1o  38857  elnev  39165  2reu8  41712
  Copyright terms: Public domain W3C validator