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

Theorem 3bitr2ri 291
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 269 . 2 (𝜑𝜒)
4 3bitr2i.3 . 2 (𝜒𝜃)
53, 4bitr2i 267 1 (𝜃𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 197
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 198
This theorem is referenced by:  xorass  1637  ssrab  3840  copsex2gb  5398  relop  5441  dmopab3  5505  dfres2  5630  restidsing  5642  idrefOLD  5692  fununi  6142  dffv2  6460  dfsup2  8557  kmlem3  9227  recmulnq  10039  nbgrel  26512  shne0i  28698  ssiun3  29759  cnvoprabOLD  29882  ind1a  30463  bnj1304  31270  bnj1253  31465  dmscut  32294  dfrecs2  32433  icorempt2  33564  inxprnres  34424  dalem20  35581  rp-isfinite6  38471  rababg  38486  ssrabf  39880
  Copyright terms: Public domain W3C validator