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

Theorem 3bitr2i 264
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 243 . 2  |-  ( ph  <->  ch )
4 3bitr2i.3 . 2  |-  ( ch  <->  th )
53, 4bitri 240 1  |-  ( ph  <->  th )
Colors of variables: wff set class
Syntax hints:    <-> wb 176
This theorem is referenced by:  con2bi  318  an13  774  xorneg1  1302  2eu5  2227  exists1  2232  euxfr  2951  rmo4  2958  2reu5lem3  2972  rmo3  3078  difin  3406  difin0ss  3520  uniuni  4527  reusv2lem4  4538  reusv6OLD  4545  reusv7OLD  4546  rabxp  4725  eliunxp  4823  imadisj  5032  intirr  5061  resco  5177  funcnv3  5311  fncnv  5314  fun11  5315  fununi  5316  mpt2mptx  5938  frxp  6225  oeeu  6601  ixp0x  6844  mapsnen  6938  xpcomco  6952  1sdom  7065  dffi3  7184  cardval3  7585  kmlem4  7779  kmlem12  7787  kmlem14  7789  kmlem15  7790  kmlem16  7791  fpwwe2  8265  axgroth4  8454  ltexprlem4  8663  bitsmod  12627  pythagtrip  12887  pgpfac1  15315  pgpfac  15319  isassa  16056  istps3OLD  16660  basdif0  16691  ntreq0  16814  tgcmp  17128  tx1cn  17303  rnelfmlem  17647  phtpcer  18493  caucfil  18709  minveclem1  18788  ovoliunlem1  18861  mdegleb  19450  adjbd1o  22665  nmo  23144  rmo3f  23178  rmo4fOLD  23179  mptfnf  23226  1stmbfm  23565  cvmlift2lem12  23845  axacprim  24053  brimg  24476  andnand1  24837  and4com  24940  fgraphopab  27529  ndmaovcom  28065  onfrALTlem5  28307  bnj976  28809  bnj1143  28822  bnj1533  28884  bnj864  28954  bnj983  28983  bnj1174  29033  bnj1175  29034  bnj1280  29050  isopos  29370  dihglblem6  31530  dihglb2  31532
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 177
  Copyright terms: Public domain W3C validator