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

Theorem 3bitr3ri 302
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 277 . 2 (𝜓𝜒)
51, 4bitr3i 277 1 (𝜃𝜒)
Colors of variables: wff setvar class
Syntax hints:  wb 205
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 206
This theorem is referenced by:  bigolden  1026  sb8f  2350  2eu8  2659  2ralorOLD  3221  sbccow  3763  sbcco  3766  dfiin2g  4993  zfpair  5377  dfpo2  6249  dffun6f  6515  fnssintima  7308  imaeqsexv  7309  fsplit  8050  axdc3lem4  10390  addsunif  27313  addsasslem1  27314  addsasslem2  27315  istrkg2ld  27405  legso  27544  disjunsn  31515  gtiso  31617  fpwrelmapffslem  31652  qqhre  32604  satfdm  33966  dfdm5  34350  dfrn5  34351  brimg  34525  dfrecs2  34538  poimirlem25  36106  cdlemefrs29bpre0  38862  cdlemftr3  39031  dffrege115  42257  brco3f1o  42312  elnev  42725  2reu8  45351  ichbi12i  45659  i0oii  46959
  Copyright terms: Public domain W3C validator