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  3044  sbcnel12g  3100  elimhyp3v  3617  elimhyp4v  3618  keephyp3v  3623  f1eq123d  5469  foeq123d  5470  f1oeq123d  5471  ofrfval  6088  eloprabi  6188  smoeq  6369  wemapwe  7402  cnfcom  7405  fseqenlem1  7653  dfac12lem2  7772  fin23lem22  7955  pwfseqlem5  8287  pwfseq  8288  enqbreq2  8546  lterpq  8596  ltdiv23  9649  lediv23  9650  halfpos  9944  addltmul  9949  supminf  10307  supxrbnd1  10642  supxrbnd2  10643  iccf1o  10780  fzshftral  10871  modirr  11011  seqcoll  11403  s111  11450  limsupgle  11953  tanaddlem  12448  dvdssub  12571  dvdsmod  12587  oddp1even  12591  bitscmp  12631  saddisjlem  12657  smueqlem  12683  prmreclem5  12969  4sqlem11  13004  4sqlem17  13010  vdwmc2  13028  ismre  13494  acsfn  13563  isssc  13699  setcinv  13924  nmzsubg  14660  conjnmzb  14719  oddvdsnn0  14861  oddvds  14864  odcong  14866  odf1  14877  dpjeq  15296  pgpfac1lem2  15312  lsmspsn  15839  lbsacsbs  15911  lpigen  16010  prmirredlem  16448  znf1o  16507  znunit  16519  isclo  16826  maxlp  16880  1stccn  17191  xkoinjcn  17383  elmptrab  17524  fbunfip  17566  elfm  17644  fmid  17657  flfnei  17688  isflf  17690  isfcls  17706  fclsopn  17711  isfcf  17731  eltsms  17817  prdsxmetlem  17934  elmopn  17990  metss  18056  comet  18061  nrmmetd  18099  metdsge  18355  tchcph  18669  fmcfil  18700  minveclem4  18798  shft2rab  18869  sca2rab  18873  volsup2  18962  mbfsup  19021  i1fmullem  19051  mbfi1fseqlem4  19075  xrge0f  19088  itg2monolem1  19107  ellimc2  19229  cnlimc  19240  mdegleb  19452  facth1  19552  ulm2  19766  sineq0  19891  coseq1  19892  efeq1  19893  sinord  19898  root1eq1  20097  angrtmuld  20108  quad2  20137  dcubic  20144  cubic2  20146  dquartlem1  20149  dquart  20151  quart  20159  rlimcnp  20262  mumullem2  20420  chtub  20453  fsumvma  20454  fsumvma2  20455  chpchtsum  20460  bposlem7  20531  lgsneg  20560  lgsne0  20574  lgsqrlem2  20583  lgsquadlem1  20595  lgsquadlem2  20596  isass  20985  rngosn3  21095  imsmetlem  21261  ipz  21297  bnsscmcl  21449  minvecolem4  21461  hvsubcan  21655  hoeq2  22413  leoptri  22718  atcv0eq  22961  fzsplit3  23033  ballotlemsima  23076  elimifd  23153  gtiso  23243  lmlim  23373  dya2ub  23577  isrrvv  23648  subfacp1lem3  23715  subfacp1lem5  23717  erdszelem1  23724  erdsze  23735  erdsze2lem2  23737  eupath2lem2  23904  eupath2lem3  23905  elpredg  24180  axcontlem7  24600  itg2addnclem2  24934  areacirclem2  24936  areacirclem3  24937  areacirclem6  24941  splint  25059  nZdef  25191  islatalg  25194  isfldOLD  25437  svli2  25495  nelioo5  25522  imonclem  25824  cmppar3  25985  isnword  25997  pdiveql  26179  filnetlem4  26341  metf1o  26480  elrfirn  26781  jm2.19lem2  27094  islinds2  27294  islindf4  27319  f1omvdconj  27400  proot1ex  27531  2reu4a  27978  isuslgra  28113  isusgra  28114  uvtx01vtx  28175  frgra3v  28191  bnj1452  29155  lsatcv0eq  29310  cmtbr2N  29516  atlatmstc  29582  1cvrco  29734  cdleme3  30499  cdleme7  30511  cdlemg10c  30901  dvhopellsm  31380  dibord  31422  dib1dim2  31431  diblsmopel  31434  dihopelvalcpre  31511  dih1dimatlem  31592  hdmap14lem13  32146  hdmapoc  32197
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