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

Theorem 3bitr2ri 292
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 270 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitr2i 268 1 (𝜃𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 198
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 199
This theorem is referenced by:  xorass  1492  ssrab  3939  copsex2gb  5529  relop  5571  dmopab3  5635  dfres2  5754  restidsing  5764  fununi  6262  dffv2  6584  dfsup2  8703  kmlem3  9372  recmulnq  10184  nbgrel  26825  shne0i  29006  ssiun3  30079  cnvoprabOLD  30215  ind1a  30928  bnj1304  31745  bnj1253  31940  dmscut  32799  dfrecs2  32938  icorempo  34080  inxprnres  34999  dalem20  36280  rp-isfinite6  39286  rababg  39301  ssrabf  40810
  Copyright terms: Public domain W3C validator