Theorem 3bitrd 287

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

Step	Hyp	Ref	Expression
1		3bitrd.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2		3bitrd.2	. . 3 |- ( ph -> ( ch <-> th ) )
3	1, 2	bitrd 261	. 2 |- ( ph -> ( ps <-> th ) )
4		3bitrd.3	. 2 |- ( ph -> ( th <-> ta ) )
5	3, 4	bitrd 261	1 |- ( ph -> ( ps <-> ta ) )

Syntax hints:   -> wi 4   <-> wb 189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 190

This theorem is referenced by:  sbceqal  3307  elimhyp3v  3932  elimhyp4v  3933  keephyp3v  3938  opelopabgf  4721  elpredg  5401  f1eq123d  5822  foeq123d  5823  f1oeq123d  5824  fnmptfvd  6000  ofrfval  6558  eloprabi  6874  fnmpt2ovd  6890  suppsnop  6947  smoeq  7087  infglbb  8025  wemapwe  8220  fseqenlem1  8473  dfac12lem2  8592  fin23lem22  8775  pwfseqlem5  9106  pwfseq  9107  enqbreq2  9363  lterpq  9413  ltdiv23  10519  lediv23  10520  negfi  10576  halfpos  10866  addltmul  10871  supminf  11273  supminfOLD  11274  supxrbnd1  11632  supxrbnd2  11633  iccf1o  11802  fzshftral  11908  fzoshftral  12053  dfceil2  12101  modirr  12194  hashen1  12588  seqcoll  12668  hash2prb  12674  s111  12806  swrdeq  12854  wrd2ind  12888  2swrd2eqwrdeq  13103  limsupgle  13612  tanaddlem  14297  dvdssub  14422  addmodlteqALT  14437  dvdsmod  14440  oddp1even  14445  bitscmp  14491  saddisjlem  14517  smueqlem  14543  ncoprmgcdne1b  14734  prmreclem5  14943  4sqlem11  14978  4sqlem17OLD  14984  4sqlem17  14990  vdwmc2  15008  ismre  15574  acsfn  15643  dfiso2  15755  brcic  15781  isssc  15803  setcinv  16063  intopsn  16576  sgrp1  16612  mnd1OLD  16656  sgrp2nmndlem4  16740  nmzsubg  16936  conjnmzb  16995  gsmsymgreqlem2  17150  symgfixels  17153  f1omvdconj  17165  oddvdsnn0  17271  oddvds  17274  odcong  17276  odf1  17291  dpjeq  17770  pgpfac1lem2  17786  ring1  17908  lsmspsn  18385  lbsacsbs  18457  lpigen  18557  prmirredlem  19141  znf1o  19199  znleval  19202  znunit  19211  islinds2  19448  islindf4  19473  scmatf1  19633  isclo  20180  maxlp  20240  1stccn  20555  xkoinjcn  20779  elmptrab  20919  fbunfip  20962  elfm  21040  fmid  21053  flfnei  21084  isflf  21086  isfcls  21102  fclsopn  21107  isfcf  21127  cnextfun  21157  eltsms  21225  prdsxmetlem  21461  elmopn  21535  metss  21601  comet  21606  elbl4  21656  metuel2  21658  nrmmetd  21667  metdsge  21944  metdsgeOLD  21959  tchcph  22289  fmcfil  22320  rrxmet  22440  minveclem4  22452  minveclem4OLD  22464  shft2rab  22539  sca2rab  22543  volsup2  22642  mbfsup  22699  i1fmullem  22731  mbfi1fseqlem4  22755  xrge0f  22768  itg2monolem1  22787  ellimc2  22911  cnlimc  22922  mdegleb  23092  facth1  23194  ulm2  23419  sineq0  23555  coseq1  23556  efeq1  23557  sinord  23562  root1eq1  23774  angrtmuld  23816  quad2  23844  dcubic  23851  cubic2  23853  dquartlem1  23856  dquart  23858  quart  23866  rlimcnp  23970  lgamucov  24042  mumullem2  24186  chtub  24219  fsumvma  24220  fsumvma2  24221  chpchtsum  24226  bposlem7  24297  lgsneg  24326  lgsne0  24340  lgsqrlem2  24349  lgsquadlem1  24361  lgsquadlem2  24362  istrkg3ld  24588  tgcgr4  24655  iscgra1  24931  isleag  24962  iseqlg  24976  axcontlem7  25079  isuslgra  25149  isusgra  25150  ausisusgra  25161  nbgraopALT  25231  nb3graprlem2  25259  cusgra3v  25271  sizeusglecusg  25293  uvtx01vtx  25299  is2wlk  25374  0pth  25379  wlkdvspthlem  25416  2wlkeq  25514  wwlknextbi  25532  clwwlkn2  25582  el2wlkonotot0  25679  el2wlkonotot  25680  el2wlksoton  25685  el2spthsoton  25686  el2wlksot  25687  el2pthsot  25688  isrusgusrgcl  25740  rusgrasn  25752  rusgranumwlkl1  25754  rusgra0edg  25762  eupath2lem2  25785  eupath2lem3  25786  frgra2v  25806  frgra3v  25809  usg2spot2nb  25872  numclwwlkovfel2  25890  numclwwlk2lem1  25909  numclwlk2lem2f1o  25912  frgrareggt1  25923  isass  26125  rngosn3  26235  imsmetlem  26403  ipz  26439  bnsscmcl  26591  minvecolem4  26603  minvecolem4OLD  26613  hvsubcan  26808  hoeq2  27565  leoptri  27870  atcv0eq  28113  elimifd  28238  gtiso  28356  2ndpreima  28363  fpwrelmapffslem  28392  fzsplit3  28445  isomnd  28538  ogrpinvlt  28561  smatrcl  28696  pstmfval  28773  lmlim  28827  dya2ub  29165  eulerpartlemr  29280  isrrvv  29349  ballotlemsima  29421  ballotlemsimaOLD  29459  signsvfn  29543  subfacp1lem3  29977  subfacp1lem5  29979  erdszelem1  29986  erdsze  29997  erdsze2lem2  29999  filnetlem4  31108  bj-issetwt  31536  bj-sbceqgALT  31572  csbwrecsg  31798  poimirlem24  32028  dvtanlemOLD  32055  itg2addnclem2  32058  ftc1anclem1  32081  areacirclem1  32096  areacirclem5  32100  metf1o  32148  lsatcv0eq  32684  cmtbr2N  32890  atlatmstc  32956  1cvrco  33108  cdleme3  33874  cdleme7  33886  cdlemg10c  34277  dvhopellsm  34756  dibord  34798  dib1dim2  34807  diblsmopel  34810  dihopelvalcpre  34887  dih1dimatlem  34968  hdmap14lem13  35522  hdmapoc  35573  elrfirn  35608  jm2.19lem2  35916  pwfi2f1o  36025  proot1ex  36149  brfvidRP  36351  bcc0  36759  pwpwuni  37456  rnmptpr  37515  disjinfi  37539  mapsnend  37551  infxrbnd2  37679  fourierdlem113  38195  isvonmbl  38578  2reu4a  38755  iccpartgtl  38885  iccpartleu  38887  iccpartgel  38888  bits0ALTV  38953  bgoldbtbndlem1  39045  pfxeq  39092  ltnltne  39191  edg0iedg0  39379  ausgrusgrb  39413  nb3grprlem2  39619  uvtxa01vtx0  39633  cplgr3v  39667  vtxd0nedgb  39711  vtxdusgr0edgnelALT  39719  1egrvtxdg0  39734  upgr2wlk  39863  1wlkp1lem8  39876  0pth-av  40014  upgriseupth  40120  eupth2lem2  40131  eupth2lem3lem4  40143  eupth2lem3lem6  40145  0nodd  40318  2nodd  40320  rngcinv  40491  rngcinvALTV  40503  ringcinv  40542  ringcinvALTV  40566  islindeps  40754  snlindsntor  40772  nn0o1gt2  40835  blen1b  40907  nn0sumshdiglem1  40940