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

Theorem 3bitr2ri 289
 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 267 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitr2i 265 1 (𝜃𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196 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 197 This theorem is referenced by:  xorass  1508  ssrab  3713  copsex2gb  5263  relop  5305  dmopab3  5369  restidsing  5493  issref  5544  fununi  6002  dffv2  6310  dfsup2  8391  kmlem3  9012  recmulnq  9824  ovoliunlem1  23316  nbgrel  26278  shne0i  28435  ssiun3  29502  cnvoprabOLD  29626  ind1a  30209  bnj1304  31016  bnj1253  31211  dmscut  32043  dfrecs2  32182  icorempt2  33329  inxprnres  34201  dalem20  35297  rp-isfinite6  38181  rababg  38196  ssrabf  39612
 Copyright terms: Public domain W3C validator