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

Theorem 3bitr2i 266
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 245 . 2  |-  ( ph  <->  ch )
4 3bitr2i.3 . 2  |-  ( ch  <->  th )
53, 4bitri 242 1  |-  ( ph  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 178
This theorem is referenced by:  con2bi  320  an13  776  xorneg1  1304  2eu5  2228  exists1  2233  euxfr  2952  rmo4  2959  2reu5lem3  2973  rmo3  3079  difin  3407  difin0ss  3521  uniuni  4526  reusv2lem4  4537  reusv6OLD  4544  reusv7OLD  4545  rabxp  4724  eliunxp  4822  imadisj  5031  intirr  5060  resco  5175  funcnv3  5276  fncnv  5279  fun11  5280  fununi  5281  mpt2mptx  5899  frxp  6186  oeeu  6596  ixp0x  6839  mapsnen  6933  xpcomco  6947  1sdom  7060  dffi3  7179  cardval3  7580  kmlem4  7774  kmlem12  7782  kmlem14  7784  kmlem15  7785  kmlem16  7786  fpwwe2  8260  axgroth4  8449  ltexprlem4  8658  bitsmod  12621  pythagtrip  12881  pgpfac1  15309  pgpfac  15313  isassa  16050  istps3OLD  16654  basdif0  16685  ntreq0  16808  tgcmp  17122  tx1cn  17297  rnelfmlem  17641  phtpcer  18487  caucfil  18703  minveclem1  18782  ovoliunlem1  18855  mdegleb  19444  adjbd1o  22657  cvmlift2lem12  23249  axacprim  23457  axfelem18  23764  brimg  23883  andnand1  24244  and4com  24338  fgraphopab  26928  ndmaovcom  27444  onfrALTlem5  27578  bnj976  28076  bnj1143  28089  bnj1533  28151  bnj864  28221  bnj983  28250  bnj1174  28300  bnj1175  28301  bnj1280  28317  isopos  28637  dihglblem6  30797  dihglb2  30799
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator