Theorem sylbi 121

Description: A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by NM, 3-Jan-1993.)

Hypotheses

Ref	Expression
sylbi.1	|- ( ph <-> ps )
sylbi.2	|- ( ps -> ch )

Assertion

Ref	Expression
sylbi	|- ( ph -> ch )

Proof of Theorem sylbi

Step	Hyp	Ref	Expression
1		sylbi.1	. . 3 |- ( ph <-> ps )
2	1	biimpi 120	. 2 |- ( ph -> ps )
3		sylbi.2	. 2 |- ( ps -> ch )
4	2, 3	syl 14	1 |- ( ph -> ch )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylbb  123  sylbb2  138  3imtr4i  201  simplbiim  387  mpan10  474  an12s  567  an32s  570  an4s  592  sylnbi  684  dcim  848  notnotrdc  850  condcOLD  861  pm2.61ddc  868  pm5.18dc  890  pm2.25dc  900  pm2.85dc  912  pm5.12dc  917  pm5.14dc  918  pm5.55dc  920  peircedc  921  pm5.54dc  925  dcand  940  dcor  943  pm5.62dc  953  pm5.63dc  954  pm4.83dc  959  ifp2  988  ifpor  995  1fpid3  1002  3simpb  1021  3simpc  1022  3imp  1219  3com12  1233  3com13  1234  syl3anb  1316  xoranor  1421  xorbin  1428  xordc1  1437  biassdc  1439  nfr  1566  nfand  1616  19.21t  1630  19.30dc  1675  exintrbi  1681  19.9t  1690  nfnt  1704  equveli  1807  exdistrfor  1848  sbcof2  1858  sbidm  1899  sbi1v  1940  sbalyz  2052  sbal1yz  2054  nfsb4t  2067  euex  2109  eumo0  2110  mor  2122  exmodc  2130  mo3h  2133  mopick  2158  moexexdc  2164  euexex  2165  2euex  2167  exists2  2177  eqcoms  2234  eleq2s  2326  nfcr  2366  necon3ai  2451  rexnalim  2521  dfrex2dc  2523  rexex  2578  rsp  2579  ralim  2591  rexim  2626  r19.32r  2679  r19.44av  2692  r19.45av  2693  gencl  2835  gencbvex  2850  gencbval  2852  vtoclgf  2862  vtoclg1f  2863  pm13.183  2944  elrabi  2959  eueq2dc  2979  eueq3dc  2980  mob2  2986  euxfr2dc  2991  reu3  2996  rmoim  3007  2rmorex  3012  sbcex  3040  sbcbi2  3082  ra5  3121  sseq1  3250  difdif  3332  dfss4st  3440  difindiss  3461  undif3ss  3468  dfrab3ss  3485  abvor0dc  3518  reldisj  3546  disjel  3549  inssdif0im  3562  uneqdifeqim  3580  r19.2m  3581  r19.2mOLD  3582  r19.3rm  3583  r19.9rmv  3586  rexm  3594  ralm  3598  raaanlem  3599  ifnefalse  3616  ifnotdc  3644  ifandc  3646  ifmdc  3648  nelpri  3693  nelprd  3695  prprc1  3780  difprsn2  3813  diftpsn3  3814  snsssn  3844  preqr2  3852  preq12b  3853  opthpr  3855  prneimg  3857  oprcl  3886  pwprss  3889  intmin4  3956  uniintabim  3965  dfiin2g  4003  iinss2  4023  iundif2ss  4036  disjnim  4078  disjnims  4079  invdisj  4081  disjiun  4083  brne0  4138  brm  4139  trel  4194  trss  4196  ssex  4226  bnd2  4263  abssexg  4272  exmidexmid  4286  rext  4307  unipw  4309  euabex  4317  mss  4318  exss  4319  copsexg  4336  opelopabsb  4354  pwssunim  4381  epelg  4387  sowlin  4417  sotritric  4421  elsuci  4500  sucprc  4509  reusv3  4557  ordon  4584  onsucmin  4605  onsucelsucr  4606  unon  4609  onsucelsucexmid  4628  setind  4637  setind2  4638  sucprcreg  4647  en2lp  4652  eunex  4659  ordsoexmid  4660  ordpwsucss  4665  tfi  4680  peano1  4692  peano2  4693  find  4697  0nelelxp  4754  opelxp  4755  elvvuni  4790  optocl  4802  ralxpf  4876  rexxpf  4877  relop  4880  breldm  4935  reldmm  4950  dmxpm  4952  elreldm  4958  dmrnssfld  4995  dmcosseq  5004  resabs1  5042  resima2  5047  issref  5119  asymref  5122  xpidtr  5127  trin2  5128  poirr2  5129  xpmlem  5157  dmxpss  5167  xp11m  5175  cnveqb  5192  dfco2a  5237  cores2  5249  coi2  5253  relcnvtr  5256  relresfld  5266  relcnvexb  5276  cnviinm  5278  iotauni  5299  iota1  5301  iota4  5306  iotam  5318  dffun8  5354  fununfun  5373  funcnvsn  5375  imadif  5410  imainlem  5411  fcoi1  5517  fcoi2  5518  f0rn0  5531  f1ocnv  5596  f1ocnvb  5597  fun11iun  5604  ffoss  5616  f1o00  5620  fo00  5621  relelfvdm  5671  nfvres  5675  nfunsn  5676  ssimaex  5707  fvmptss2  5721  fvmptssdm  5731  unpreima  5772  respreima  5775  elrnrexdm  5786  elrnrexdmb  5787  rexrnmpt  5790  dffo4  5795  rnmptss  5808  funiun  5828  funopdmsn  5833  fvpr1  5857  fvpr2  5858  elunirn  5906  f1veqaeq  5909  isores1  5954  iotaexel  5975  riotauni  5977  riotacl2  5985  riota1  5990  riota1a  5991  snriota  6002  eusvobj2  6003  acexmidlema  6008  acexmidlemb  6009  acexmidlem2  6014  oprabid  6049  0neqopab  6065  brabvv  6066  1stval2  6317  2ndval2  6318  xp1st  6327  xp2nd  6328  unielxp  6336  releldm2  6347  cnvf1o  6389  fo2ndf  6391  poxp  6396  reldmtpos  6418  dftpos4  6428  tpostpos  6429  tpostpos2  6430  iunon  6449  smoel  6465  tfrlem4  6478  tfrlem7  6482  tfrlem8  6483  tfrlem9  6484  nnaord  6676  ecexr  6706  swoord1  6730  swoord2  6731  0er  6735  mapprc  6820  mapsnconst  6862  ixpf  6888  mptelixpg  6902  idssen  6949  ener  6952  en0  6968  en1  6972  en1bg  6973  2dom  6979  modom  6993  enm  7003  xpsnen  7004  ssenen  7036  snnen2og  7044  php5dom  7048  phpm  7051  findcard  7076  findcard2  7077  findcard2s  7078  unfiexmid  7109  fiintim  7122  fidcenumlemim  7150  sbthlem1  7155  fiss  7175  djuexb  7242  djuss  7268  eldju2ndl  7270  eldju2ndr  7271  ctssdclemr  7310  exmidlpo  7341  finnum  7386  ficardon  7392  exmidfodomrlemim  7411  acnrcl  7415  3nsssucpw1  7453  indpi  7561  subhalfnqq  7633  archnqq  7636  enq0sym  7651  nqnq0pi  7657  nqnq0  7660  mulnnnq0  7669  prml  7696  prmu  7697  prssnql  7698  prssnqu  7699  prcdnql  7703  prcunqu  7704  prltlu  7706  prnmaxl  7707  prnminu  7708  prloc  7710  prdisj  7711  addcanprg  7835  recexprlemopl  7844  recexprlemopu  7846  cauappcvgprlemladdfu  7873  caucvgprlemladdfu  7896  recexgt0sr  7992  renfdisj  8238  axsuploc  8251  negf1o  8560  recexre  8757  apsqgt0  8780  apreim  8782  aprcl  8825  recexaplem2  8831  rerecclap  8909  nn0ge0  9426  elnnnn0b  9445  xnn0xr  9469  xnn0nemnf  9475  xnn0nnn0pnf  9477  znegcl  9509  zeo  9584  nn0ind  9593  nn0ind-raph  9596  uzn0  9771  eluzaddi  9782  eluzsubi  9783  uznn0sub  9787  uz3m2nn  9806  uznnssnn  9810  uz2m1nn  9838  uz2mulcl  9841  indstr2  9842  qmulz  9856  qre  9858  qnegcl  9869  qreccl  9875  rphalflt  9917  nn0ledivnn  10001  xrltnr  10013  nltpnft  10048  ngtmnft  10051  xrrebnd  10053  xnegcl  10066  xnegneg  10067  xltnegi  10069  xrpnfdc  10076  xrmnfdc  10077  xnegid  10093  xaddid1  10096  xnn0lenn0nn0  10099  xnn0xadd0  10101  xposdif  10116  elioore  10146  elfzuz2  10263  uzsubsubfz  10281  fzdisj  10286  fzmmmeqm  10292  elfz0ubfz0  10359  elfz0fzfz0  10360  fz0fzelfz0  10361  fz0fzdiffz0  10364  elfzmlbp  10366  difelfzle  10368  difelfznle  10369  nn0disj  10372  2ffzeq  10375  fzo1fzo0n0  10421  elfzo0z  10422  elfzo0le  10423  fzonmapblen  10425  fzofzim  10426  elfzodifsumelfzo  10445  elfzonlteqm1  10454  fzonn0p1p1  10457  elfzom1p1elfzo  10458  ssfzo12bi  10469  ubmelm1fzo  10470  fzind2  10484  subfzo0  10487  infssuzcldc  10494  rebtwn2z  10513  fldiv4p1lem1div2  10564  fldiv4lem1div2  10566  flqeqceilz  10579  zmodidfzoimp  10615  modfzo0difsn  10656  nnsinds  10706  nn0sinds  10707  expcl2lemap  10812  qexpclz  10821  zzlesq  10969  facp1  10991  facnn2  10995  faclbnd3  11004  bcn1  11019  hashfz0  11088  wrdf  11118  swrdswrdlem  11284  swrdswrd  11285  swrdccatin1  11305  pfxccatin12lem2a  11307  pfxccatin12lem1  11308  swrdccatin2  11309  pfxccatin12lem2  11311  pfxccatin12lem3  11312  pfxccatin12  11313  pfxccat3  11314  swrdccat  11315  swrdccat3blem  11319  cvg1nlemres  11545  rexanuz  11548  fclim  11854  climmo  11858  iser3shft  11906  fsumsplitsn  11970  fsum2dlemstep  11994  fisumcom2  11998  arisum  12058  arisum2  12059  prodmodc  12138  fprodfac  12175  fprod2dlemstep  12182  fprodcom2fi  12186  fprodsplitsn  12193  eftlub  12250  ef01bndlem  12316  sin01gt0  12322  cos01gt0  12323  sin02gt0  12324  dvdsdivcl  12410  addmodlteqALT  12419  odd2np1  12433  oddge22np1  12441  m1expe  12459  nn0enne  12462  nn0o1gt2  12465  nno  12466  ndvdsadd  12491  dfgcd2  12584  mulgcd  12586  algfx  12623  prmind2  12691  prm2orodd  12697  prmgt1  12703  oddprmgt2  12705  dfphi2  12791  nnnn0modprm0  12827  prm23lt5  12835  pythagtriplem2  12838  pcz  12904  dvdsprmpweqnn  12908  oddprmdvds  12926  prmunb  12934  4sqlem4  12964  4sqlem19  12981  evenennn  13013  fngsum  13470  igsumvalx  13471  dfgrp3me  13682  mulgnn0gsum  13714  rngdi  13952  rngdir  13953  dvdsrcl2  14112  unitinvcl  14136  unitinvinv  14137  unitlinv  14139  unitrinv  14140  rmodislmodlem  14363  rmodislmod  14364  zrhval  14630  psrbagf  14683  distop  14808  ntrss  14842  ssntr  14845  lmrcl  14915  txuni2  14979  txcn  14998  hmeocnvb  15041  xmetunirn  15081  blssioo  15276  divcnap  15288  cdivcncfap  15327  dedekindeulemlub  15343  dedekindicclemlub  15352  dvexp2  15435  elply2  15458  plyco  15482  pilem3  15506  sincosq1sgn  15549  sincosq2sgn  15550  sincosq3sgn  15551  sincosq4sgn  15552  sinq12gt0  15553  fsumdvdsmul  15714  zabsle1  15727  lgsdir2lem4  15759  gausslemma2dlem0f  15782  gausslemma2dlem1a  15786  gausslemma2dlem2  15790  gausslemma2dlem3  15791  gausslemma2dlem4  15792  2lgslem1a1  15814  2lgslem3  15829  2lgsoddprmlem3  15839  2lgsoddprm  15841  2sqlem2  15843  2sqlem10  15853  vtxvalprc  15905  iedgvalprc  15906  upgrex  15953  umgredg  15995  ausgrusgrben  16018  usgruspgrben  16036  usgrislfuspgrdom  16040  uhgr2edg  16056  uspgredg2v  16071  griedg0ssusgr  16101  subusgr  16125  wlkv  16176  wlk1walkdom  16209  trlsv  16234  trlf1  16238  clwwlk1loop  16249  clwwlkext2edg  16272  umgr2cwwkdifex  16275  clwwlknonex2lem2  16288  clwwlknonex2e  16290  eupthv  16296  bj-pm2.18st  16346  bj-dcstab  16352  decidi  16391  sumdc2  16395  bj-charfunbi  16406  bdel  16440  bdssex  16497  bj-indind  16527  findset  16540  nninfall  16611  trirec0  16648  neap0mkv  16673