MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3bitr2i Structured version   Unicode version

Theorem 3bitr2i 265
Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr2i.1  |-  ( ph  <->  ps )
3bitr2i.2  |-  ( ch  <->  ps )
3bitr2i.3  |-  ( ch  <->  th )
Assertion
Ref Expression
3bitr2i  |-  ( ph  <->  th )

Proof of Theorem 3bitr2i
StepHypRef Expression
1 3bitr2i.1 . . 3  |-  ( ph  <->  ps )
2 3bitr2i.2 . . 3  |-  ( ch  <->  ps )
31, 2bitr4i 244 . 2  |-  ( ph  <->  ch )
4 3bitr2i.3 . 2  |-  ( ch  <->  th )
53, 4bitri 241 1  |-  ( ph  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 177
This theorem is referenced by:  con2bi  319  an13  775  xorneg1  1320  2eu5  2364  exists1  2369  euxfr  3112  euind  3113  rmo4  3119  2reu5lem3  3133  rmo3  3240  difin  3570  difin0ss  3686  uniuni  4708  reusv2lem4  4719  reusv6OLD  4726  reusv7OLD  4727  rabxp  4906  eliunxp  5004  imadisj  5215  intirr  5244  resco  5366  funcnv3  5504  fncnv  5507  fun11  5508  fununi  5509  f1mpt  5999  mpt2mptx  6156  frxp  6448  oeeu  6838  ixp0x  7082  mapsnen  7176  xpcomco  7190  1sdom  7303  dffi3  7428  cardval3  7829  kmlem4  8023  kmlem12  8031  kmlem14  8033  kmlem15  8034  kmlem16  8035  fpwwe2  8508  axgroth4  8697  ltexprlem4  8906  bitsmod  12938  pythagtrip  13198  pgpfac1  15628  pgpfac  15632  isassa  16365  istps3OLD  16977  basdif0  17008  ntreq0  17131  tgcmp  17454  tx1cn  17631  rnelfmlem  17974  phtpcer  19010  caucfil  19226  minveclem1  19315  ovoliunlem1  19388  mdegleb  19977  3v3e3cycl2  21641  adjbd1o  23578  nmo  23963  rmo3f  23972  rmo4fOLD  23973  mptfnf  24063  1stmbfm  24600  cvmlift2lem12  24991  axacprim  25146  andnand1  26113  itg2addnc  26222  fgraphopab  27461  ndmaovcom  28000  usgra2pth0  28229  onfrALTlem5  28529  bnj976  29049  bnj1143  29062  bnj1533  29124  bnj864  29194  bnj983  29223  bnj1174  29273  bnj1175  29274  bnj1280  29290  isopos  29879  dihglblem6  32039  dihglb2  32041
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator