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

Theorem 3bitr3ri 290
 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 265 . 2 (𝜓𝜒)
51, 4bitr3i 265 1 (𝜃𝜒)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195 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 196 This theorem is referenced by:  bigolden  972  2eu8  2548  2ralor  3088  sbcco  3425  symdifass  3815  dfiin2g  4489  zfpair  4831  dffun6f  5818  fsplit  7169  axdc3lem4  9158  istrkg2ld  25159  legso  25294  disjunsn  28789  gtiso  28861  fpwrelmapffslem  28895  qqhre  29392  dfpo2  30898  dfdm5  30921  dfrn5  30922  nofulllem5  31105  brimg  31214  dfrecs2  31227  poimirlem25  32604  cdlemefrs29bpre0  34702  cdlemftr3  34871  dffrege115  37292  brco3f1o  37351  elnev  37661  2reu8  39841
 Copyright terms: Public domain W3C validator