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  cvmlift2lem12  23256  axacprim  23464  brimg  23887  andnand1  24248  and4com  24352  fgraphopab  26941  ndmaovcom  27477  onfrALTlem5  27680  bnj976  28182  bnj1143  28195  bnj1533  28257  bnj864  28327  bnj983  28356  bnj1174  28406  bnj1175  28407  bnj1280  28423  isopos  28743  dihglblem6  30903  dihglb2  30905
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