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

Theorem 3bitrd 271
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 245 . 2  |-  ( ph  ->  ( ps  <->  th )
)
4 3bitrd.3 . 2  |-  ( ph  ->  ( th  <->  ta )
)
53, 4bitrd 245 1  |-  ( ph  ->  ( ps  <->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  sbceqal  3156  sbcnel12g  3212  elimhyp3v  3733  elimhyp4v  3734  keephyp3v  3739  f1eq123d  5610  foeq123d  5611  f1oeq123d  5612  ofrfval  6253  eloprabi  6353  smoeq  6549  wemapwe  7588  fseqenlem1  7839  dfac12lem2  7958  fin23lem22  8141  pwfseqlem5  8472  pwfseq  8473  enqbreq2  8731  lterpq  8781  ltdiv23  9834  lediv23  9835  halfpos  10131  addltmul  10136  supminf  10496  supxrbnd1  10833  supxrbnd2  10834  iccf1o  10972  fzshftral  11065  modirr  11214  seqcoll  11640  s111  11690  limsupgle  12199  tanaddlem  12695  dvdssub  12818  dvdsmod  12834  oddp1even  12838  bitscmp  12878  saddisjlem  12904  smueqlem  12930  prmreclem5  13216  4sqlem11  13251  4sqlem17  13257  vdwmc2  13275  ismre  13743  acsfn  13812  isssc  13948  setcinv  14173  nmzsubg  14909  conjnmzb  14968  oddvdsnn0  15110  oddvds  15113  odcong  15115  odf1  15126  dpjeq  15545  pgpfac1lem2  15561  lsmspsn  16084  lbsacsbs  16156  lpigen  16255  prmirredlem  16697  znf1o  16756  znunit  16768  isclo  17075  maxlp  17134  1stccn  17448  xkoinjcn  17641  elmptrab  17781  fbunfip  17823  elfm  17901  fmid  17914  flfnei  17945  isflf  17947  isfcls  17963  fclsopn  17968  isfcf  17988  cnextfun  18017  eltsms  18084  prdsxmetlem  18307  elmopn  18363  metss  18429  comet  18434  elbl4  18484  metuel2  18486  nrmmetd  18494  metdsge  18751  tchcph  19066  fmcfil  19097  minveclem4  19201  shft2rab  19272  sca2rab  19276  volsup2  19365  mbfsup  19424  i1fmullem  19454  mbfi1fseqlem4  19478  xrge0f  19491  itg2monolem1  19510  ellimc2  19632  cnlimc  19643  mdegleb  19855  facth1  19955  ulm2  20169  sineq0  20297  coseq1  20298  efeq1  20299  sinord  20304  root1eq1  20507  angrtmuld  20518  quad2  20547  dcubic  20554  cubic2  20556  dquartlem1  20559  dquart  20561  quart  20569  rlimcnp  20672  mumullem2  20831  chtub  20864  fsumvma  20865  fsumvma2  20866  chpchtsum  20871  bposlem7  20942  lgsneg  20971  lgsne0  20985  lgsqrlem2  20994  lgsquadlem1  21006  lgsquadlem2  21007  isuslgra  21240  isusgra  21241  ausisusgra  21248  nb3graprlem2  21328  cusgra3v  21340  sizeusglecusg  21362  uvtx01vtx  21368  0pth  21425  wlkdvspthlem  21456  eupath2lem2  21549  eupath2lem3  21550  isass  21753  rngosn3  21863  imsmetlem  22031  ipz  22067  bnsscmcl  22219  minvecolem4  22231  hvsubcan  22425  hoeq2  23183  leoptri  23488  atcv0eq  23731  elimifd  23849  gtiso  23930  2ndpreima  23938  fzsplit3  23987  isofld  24062  lmlim  24138  dya2ub  24415  isrrvv  24481  ballotlemsima  24553  lgamucov  24602  subfacp1lem3  24648  subfacp1lem5  24650  erdszelem1  24657  erdsze  24668  erdsze2lem2  24670  elpredg  25203  axcontlem7  25624  itg2addnclem2  25959  areacirclem2  25983  areacirclem3  25984  areacirclem6  25988  filnetlem4  26102  metf1o  26153  elrfirn  26441  jm2.19lem2  26753  islinds2  26953  islindf4  26978  f1omvdconj  27059  proot1ex  27190  2reu4a  27636  frgra3v  27756  bnj1452  28760  lsatcv0eq  29163  cmtbr2N  29369  atlatmstc  29435  1cvrco  29587  cdleme3  30352  cdleme7  30364  cdlemg10c  30754  dvhopellsm  31233  dibord  31275  dib1dim2  31284  diblsmopel  31287  dihopelvalcpre  31364  dih1dimatlem  31445  hdmap14lem13  31999  hdmapoc  32050
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 178
  Copyright terms: Public domain W3C validator