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

Theorem 3bitr3ri 305
 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 280 . 2 (𝜓𝜒)
51, 4bitr3i 280 1 (𝜃𝜒)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209 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 210 This theorem is referenced by:  bigolden  1024  2eu8  2721  2ralor  3322  sbccow  3743  sbcco  3746  dfiin2g  4920  zfpair  5288  dffun6f  6339  fsplit  7798  fsplitOLD  7799  axdc3lem4  9867  istrkg2ld  26264  legso  26403  disjunsn  30367  gtiso  30470  fpwrelmapffslem  30504  qqhre  31386  satfdm  32744  dfpo2  33119  dfdm5  33144  dfrn5  33145  brimg  33526  dfrecs2  33539  poimirlem25  35101  cdlemefrs29bpre0  37711  cdlemftr3  37880  dffrege115  40722  brco3f1o  40779  elnev  41185  2reu8  43711  ichbi12i  44020
 Copyright terms: Public domain W3C validator