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

Theorem 3bitrd 270
Description: Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.)
Hypotheses
Ref Expression
3bitrd.1  |-  ( ph  ->  ( ps  <->  ch )
)
3bitrd.2  |-  ( ph  ->  ( ch  <->  th )
)
3bitrd.3  |-  ( ph  ->  ( th  <->  ta )
)
Assertion
Ref Expression
3bitrd  |-  ( ph  ->  ( ps  <->  ta )
)

Proof of Theorem 3bitrd
StepHypRef Expression
1 3bitrd.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
2 3bitrd.2 . . 3  |-  ( ph  ->  ( ch  <->  th )
)
31, 2bitrd 244 . 2  |-  ( ph  ->  ( ps  <->  th )
)
4 3bitrd.3 . 2  |-  ( ph  ->  ( th  <->  ta )
)
53, 4bitrd 244 1  |-  ( ph  ->  ( ps  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  sbceqal  3042  sbcnel12g  3098  elimhyp3v  3615  elimhyp4v  3616  keephyp3v  3621  f1eq123d  5467  foeq123d  5468  f1oeq123d  5469  ofrfval  6086  eloprabi  6186  smoeq  6367  wemapwe  7400  cnfcom  7403  fseqenlem1  7651  dfac12lem2  7770  fin23lem22  7953  pwfseqlem5  8285  pwfseq  8286  enqbreq2  8544  lterpq  8594  ltdiv23  9647  lediv23  9648  halfpos  9942  addltmul  9947  supminf  10305  supxrbnd1  10640  supxrbnd2  10641  iccf1o  10778  fzshftral  10869  modirr  11009  seqcoll  11401  s111  11448  limsupgle  11951  tanaddlem  12446  dvdssub  12569  dvdsmod  12585  oddp1even  12589  bitscmp  12629  saddisjlem  12655  smueqlem  12681  prmreclem5  12967  4sqlem11  13002  4sqlem17  13008  vdwmc2  13026  ismre  13492  acsfn  13561  isssc  13697  setcinv  13922  nmzsubg  14658  conjnmzb  14717  oddvdsnn0  14859  oddvds  14862  odcong  14864  odf1  14875  dpjeq  15294  pgpfac1lem2  15310  lsmspsn  15837  lbsacsbs  15909  lpigen  16008  prmirredlem  16446  znf1o  16505  znunit  16517  isclo  16824  maxlp  16878  1stccn  17189  xkoinjcn  17381  elmptrab  17522  fbunfip  17564  elfm  17642  fmid  17655  flfnei  17686  isflf  17688  isfcls  17704  fclsopn  17709  isfcf  17729  eltsms  17815  prdsxmetlem  17932  elmopn  17988  metss  18054  comet  18059  nrmmetd  18097  metdsge  18353  tchcph  18667  fmcfil  18698  minveclem4  18796  shft2rab  18867  sca2rab  18871  volsup2  18960  mbfsup  19019  i1fmullem  19049  mbfi1fseqlem4  19073  xrge0f  19086  itg2monolem1  19105  ellimc2  19227  cnlimc  19238  mdegleb  19450  facth1  19550  ulm2  19764  sineq0  19889  coseq1  19890  efeq1  19891  sinord  19896  root1eq1  20095  angrtmuld  20106  quad2  20135  dcubic  20142  cubic2  20144  dquartlem1  20147  dquart  20149  quart  20157  rlimcnp  20260  mumullem2  20418  chtub  20451  fsumvma  20452  fsumvma2  20453  chpchtsum  20458  bposlem7  20529  lgsneg  20558  lgsne0  20572  lgsqrlem2  20581  lgsquadlem1  20593  lgsquadlem2  20594  isass  20983  rngosn3  21093  imsmetlem  21259  ipz  21295  bnsscmcl  21447  minvecolem4  21459  hvsubcan  21653  hoeq2  22411  leoptri  22716  atcv0eq  22959  fzsplit3  23031  ballotlemsima  23074  elimifd  23151  gtiso  23241  lmlim  23371  dya2ub  23575  isrrvv  23646  subfacp1lem3  23713  subfacp1lem5  23715  erdszelem1  23722  erdsze  23733  erdsze2lem2  23735  eupath2lem2  23902  eupath2lem3  23903  elpredg  24178  axcontlem7  24598  areacirclem2  24925  areacirclem3  24926  areacirclem6  24930  splint  25048  nZdef  25180  islatalg  25183  isfldOLD  25426  svli2  25484  nelioo5  25511  imonclem  25813  cmppar3  25974  isnword  25986  pdiveql  26168  filnetlem4  26330  metf1o  26469  elrfirn  26770  jm2.19lem2  27083  islinds2  27283  islindf4  27308  f1omvdconj  27389  proot1ex  27520  2reu4a  27967  isuslgra  28102  isusgra  28103  uvtx01vtx  28164  frgra3v  28180  bnj1452  29082  lsatcv0eq  29237  cmtbr2N  29443  atlatmstc  29509  1cvrco  29661  cdleme3  30426  cdleme7  30438  cdlemg10c  30828  dvhopellsm  31307  dibord  31349  dib1dim2  31358  diblsmopel  31361  dihopelvalcpre  31438  dih1dimatlem  31519  hdmap14lem13  32073  hdmapoc  32124
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