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  777  xorneg1  1307  2eu5  2200  exists1  2205  euxfr  2919  rmo4  2926  rmo3  3039  difin  3367  difin0ss  3481  uniuni  4485  reusv2lem4  4496  reusv6OLD  4503  reusv7OLD  4504  rabxp  4699  eliunxp  4797  imadisj  5006  intirr  5035  resco  5150  funcnv3  5235  fncnv  5238  fun11  5239  fununi  5240  mpt2mptx  5858  frxp  6145  oeeu  6555  ixp0x  6798  mapsnen  6892  xpcomco  6906  1sdom  7019  dffi3  7138  cardval3  7539  kmlem4  7733  kmlem12  7741  kmlem14  7743  kmlem15  7744  kmlem16  7745  fpwwe2  8219  axgroth4  8408  ltexprlem4  8617  bitsmod  12575  pythagtrip  12835  pgpfac1  15263  pgpfac  15267  isassa  16004  istps3OLD  16608  basdif0  16639  ntreq0  16762  tgcmp  17076  tx1cn  17251  rnelfmlem  17595  phtpcer  18441  caucfil  18657  minveclem1  18736  ovoliunlem1  18809  mdegleb  19398  adjbd1o  22611  cvmlift2lem12  23203  axacprim  23411  axfelem18  23718  brimg  23837  andnand1  24198  and4com  24292  fgraphopab  26882  onfrALTlem5  27344  bnj976  27842  bnj1143  27855  bnj1533  27917  bnj864  27987  bnj983  28016  bnj1174  28066  bnj1175  28067  bnj1280  28083  isopos  28521  dihglblem6  30681  dihglb2  30683
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