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

Theorem 3bitr2ri 287
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 265 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitr2i 263 1 (𝜃𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 194
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 195
This theorem is referenced by:  xorass  1459  ssrab  3642  copsex2gb  5141  relop  5181  dmopab3  5245  restidsing  5363  issref  5414  fununi  5863  dffv2  6165  dfsup2  8210  kmlem3  8834  recmulnq  9642  ovoliunlem1  23021  shne0i  27484  ssiun3  28552  cnvoprab  28679  ind1a  29203  bnj1304  29937  bnj1253  30132  dfrecs2  31020  icorempt2  32158  dalem20  33780  rp-isfinite6  36666  rababg  36681  ssrabf  38112
  Copyright terms: Public domain W3C validator