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

Theorem 3bitr2ri 300
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 278 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitr2i 276 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:  xorass  1515  ssrab  4035  copsex2gb  5767  relop  5811  dmopab3  5880  dfres2  6000  restidsing  6011  fununi  6581  dffv2  6941  dfsup2  9387  kmlem3  10095  recmulnq  10907  dmscut  27172  nbgrel  28330  shne0i  30432  13an22anass  31437  ssiun3  31519  cnvoprabOLD  31679  ind1a  32658  bnj1304  33471  bnj1253  33669  dfrecs2  34564  icorempo  35851  inxprnres  36782  disjressuc2  36879  dalem20  38185  ralopabb  41757  rp-isfinite6  41864  rababg  41920  ssrabf  43398  ralfal  43450
  Copyright terms: Public domain W3C validator