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

Theorem 3bitr2ri 303
 Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr2i.1 (𝜑𝜓)
3bitr2i.2 (𝜒𝜓)
3bitr2i.3 (𝜒𝜃)
Assertion
Ref Expression
3bitr2ri (𝜃𝜑)

Proof of Theorem 3bitr2ri
StepHypRef Expression
1 3bitr2i.1 . . 3 (𝜑𝜓)
2 3bitr2i.2 . . 3 (𝜒𝜓)
31, 2bitr4i 281 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitr2i 279 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:  xorass  1507  nororOLD  1530  ssrab  4001  copsex2gb  5646  relop  5688  dmopab3  5757  dfres2  5879  restidsing  5892  fununi  6404  dffv2  6740  dfsup2  8907  kmlem3  9578  recmulnq  10390  nbgrel  27171  shne0i  29272  ssiun3  30363  cnvoprabOLD  30523  ind1a  31451  bnj1304  32264  bnj1253  32462  dmscut  33448  dfrecs2  33587  icorempo  34835  inxprnres  35776  dalem20  37056  rp-isfinite6  40313  rababg  40360  ssrabf  41837
 Copyright terms: Public domain W3C validator