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  3155  sbcnel12g  3211  elimhyp3v  3732  elimhyp4v  3733  keephyp3v  3738  f1eq123d  5609  foeq123d  5610  f1oeq123d  5611  ofrfval  6252  eloprabi  6352  smoeq  6548  wemapwe  7587  fseqenlem1  7838  dfac12lem2  7957  fin23lem22  8140  pwfseqlem5  8471  pwfseq  8472  enqbreq2  8730  lterpq  8780  ltdiv23  9833  lediv23  9834  halfpos  10130  addltmul  10135  supminf  10495  supxrbnd1  10832  supxrbnd2  10833  iccf1o  10971  fzshftral  11064  modirr  11213  seqcoll  11639  s111  11689  limsupgle  12198  tanaddlem  12694  dvdssub  12817  dvdsmod  12833  oddp1even  12837  bitscmp  12877  saddisjlem  12903  smueqlem  12929  prmreclem5  13215  4sqlem11  13250  4sqlem17  13256  vdwmc2  13274  ismre  13742  acsfn  13811  isssc  13947  setcinv  14172  nmzsubg  14908  conjnmzb  14967  oddvdsnn0  15109  oddvds  15112  odcong  15114  odf1  15125  dpjeq  15544  pgpfac1lem2  15560  lsmspsn  16083  lbsacsbs  16155  lpigen  16254  prmirredlem  16696  znf1o  16755  znunit  16767  isclo  17074  maxlp  17133  1stccn  17447  xkoinjcn  17640  elmptrab  17780  fbunfip  17822  elfm  17900  fmid  17913  flfnei  17944  isflf  17946  isfcls  17962  fclsopn  17967  isfcf  17987  cnextfun  18016  eltsms  18083  prdsxmetlem  18306  elmopn  18362  metss  18428  comet  18433  elbl4  18483  metuel2  18485  nrmmetd  18493  metdsge  18750  tchcph  19065  fmcfil  19096  minveclem4  19200  shft2rab  19271  sca2rab  19275  volsup2  19364  mbfsup  19423  i1fmullem  19453  mbfi1fseqlem4  19477  xrge0f  19490  itg2monolem1  19509  ellimc2  19631  cnlimc  19642  mdegleb  19854  facth1  19954  ulm2  20168  sineq0  20296  coseq1  20297  efeq1  20298  sinord  20303  root1eq1  20506  angrtmuld  20517  quad2  20546  dcubic  20553  cubic2  20555  dquartlem1  20558  dquart  20560  quart  20568  rlimcnp  20671  mumullem2  20830  chtub  20863  fsumvma  20864  fsumvma2  20865  chpchtsum  20870  bposlem7  20941  lgsneg  20970  lgsne0  20984  lgsqrlem2  20993  lgsquadlem1  21005  lgsquadlem2  21006  isuslgra  21239  isusgra  21240  ausisusgra  21247  nb3graprlem2  21327  cusgra3v  21339  sizeusglecusg  21361  uvtx01vtx  21367  0pth  21424  wlkdvspthlem  21455  eupath2lem2  21548  eupath2lem3  21549  isass  21752  rngosn3  21862  imsmetlem  22030  ipz  22066  bnsscmcl  22218  minvecolem4  22230  hvsubcan  22424  hoeq2  23182  leoptri  23487  atcv0eq  23730  elimifd  23848  gtiso  23929  2ndpreima  23937  fzsplit3  23986  isofld  24061  lmlim  24137  dya2ub  24414  isrrvv  24480  ballotlemsima  24552  lgamucov  24601  subfacp1lem3  24647  subfacp1lem5  24649  erdszelem1  24656  erdsze  24667  erdsze2lem2  24669  elpredg  25202  axcontlem7  25623  itg2addnclem2  25958  areacirclem2  25982  areacirclem3  25983  areacirclem6  25987  filnetlem4  26101  metf1o  26152  elrfirn  26440  jm2.19lem2  26752  islinds2  26952  islindf4  26977  f1omvdconj  27058  proot1ex  27189  2reu4a  27635  frgra3v  27755  bnj1452  28759  lsatcv0eq  29162  cmtbr2N  29368  atlatmstc  29434  1cvrco  29586  cdleme3  30351  cdleme7  30363  cdlemg10c  30753  dvhopellsm  31232  dibord  31274  dib1dim2  31283  diblsmopel  31286  dihopelvalcpre  31363  dih1dimatlem  31444  hdmap14lem13  31998  hdmapoc  32049
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