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  685  dcim  849  notnotrdc  851  condcOLD  862  pm2.61ddc  869  pm5.18dc  891  pm2.25dc  901  pm2.85dc  913  pm5.12dc  918  pm5.14dc  919  pm5.55dc  921  peircedc  922  pm5.54dc  926  dcand  941  dcor  944  pm5.62dc  954  pm5.63dc  955  pm4.83dc  960  ifp2  989  ifpor  996  1fpid3  1003  3simpb  1022  3simpc  1023  3imp  1220  3com12  1234  3com13  1235  syl3anb  1317  xoranor  1422  xorbin  1429  xordc1  1438  biassdc  1440  nfr  1567  nfand  1617  19.21t  1631  19.30dc  1676  exintrbi  1682  19.9t  1691  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  2367  necon3ai  2452  rexnalim  2522  dfrex2dc  2524  rexex  2579  rsp  2580  ralim  2592  rexim  2627  r19.32r  2680  r19.44av  2693  r19.45av  2694  gencl  2836  gencbvex  2851  gencbval  2853  vtoclgf  2863  vtoclg1f  2864  pm13.183  2945  elrabi  2960  eueq2dc  2980  eueq3dc  2981  mob2  2987  euxfr2dc  2992  reu3  2997  rmoim  3008  2rmorex  3013  sbcex  3041  sbcbi2  3083  ra5  3122  sseq1  3251  difdif  3334  dfss4st  3442  difindiss  3463  undif3ss  3470  dfrab3ss  3487  abvor0dc  3520  reldisj  3548  disjel  3551  inssdif0im  3564  uneqdifeqim  3582  r19.2m  3583  r19.2mOLD  3584  r19.3rm  3585  r19.9rmv  3588  rexm  3596  ralm  3600  raaanlem  3601  ifnefalse  3620  ifnotdc  3648  ifandc  3650  ifmdc  3652  nelpri  3697  nelprd  3699  prprc1  3784  difprsn2  3818  diftpsn3  3819  snsssn  3849  preqr2  3857  preq12b  3858  opthpr  3860  prneimg  3862  oprcl  3891  pwprss  3894  intmin4  3961  uniintabim  3970  dfiin2g  4008  iinss2  4028  iundif2ss  4041  disjnim  4083  disjnims  4084  invdisj  4086  disjiun  4088  brne0  4143  brm  4144  trel  4199  trss  4201  ssex  4231  bnd2  4269  abssexg  4278  exmidexmid  4292  rext  4313  unipw  4315  euabex  4323  mss  4324  exss  4325  copsexg  4342  opelopabsb  4360  pwssunim  4387  epelg  4393  sowlin  4423  sotritric  4427  elsuci  4506  sucprc  4515  reusv3  4563  ordon  4590  onsucmin  4611  onsucelsucr  4612  unon  4615  onsucelsucexmid  4634  setind  4643  setind2  4644  sucprcreg  4653  en2lp  4658  eunex  4665  ordsoexmid  4666  ordpwsucss  4671  tfi  4686  peano1  4698  peano2  4699  find  4703  0nelelxp  4760  opelxp  4761  elvvuni  4796  optocl  4808  ralxpf  4882  rexxpf  4883  relop  4886  breldm  4941  reldmm  4956  dmxpm  4958  elreldm  4964  dmrnssfld  5001  dmcosseq  5010  resabs1  5048  resima2  5053  issref  5126  asymref  5129  xpidtr  5134  trin2  5135  poirr2  5136  xpmlem  5164  dmxpss  5174  xp11m  5182  cnveqb  5199  dfco2a  5244  cores2  5256  coi2  5260  relcnvtr  5263  relresfld  5273  relcnvexb  5283  cnviinm  5285  iotauni  5306  iota1  5308  iota4  5313  iotam  5325  dffun8  5361  fununfun  5380  funcnvsn  5382  imadif  5417  imainlem  5418  fcoi1  5525  fcoi2  5526  f0rn0  5540  f1ocnv  5605  f1ocnvb  5606  fun11iun  5613  ffoss  5625  f1o00  5629  fo00  5630  relelfvdm  5680  nfvres  5684  nfunsn  5685  ssimaex  5716  fvmptss2  5730  fvmptssdm  5740  unpreima  5780  respreima  5783  elrnrexdm  5794  elrnrexdmb  5795  rexrnmpt  5798  dffo4  5803  rnmptss  5816  funiun  5837  funopdmsn  5842  fvpr1  5866  fvpr2  5867  elunirn  5917  f1veqaeq  5920  isores1  5965  iotaexel  5986  riotauni  5988  riotacl2  5996  riota1  6001  riota1a  6002  snriota  6013  eusvobj2  6014  acexmidlema  6019  acexmidlemb  6020  acexmidlem2  6025  oprabid  6060  0neqopab  6076  brabvv  6077  1stval2  6327  2ndval2  6328  xp1st  6337  xp2nd  6338  unielxp  6346  releldm2  6357  cnvf1o  6399  fo2ndf  6401  poxp  6406  reldmtpos  6462  dftpos4  6472  tpostpos  6473  tpostpos2  6474  iunon  6493  smoel  6509  tfrlem4  6522  tfrlem7  6526  tfrlem8  6527  tfrlem9  6528  nnaord  6720  ecexr  6750  swoord1  6774  swoord2  6775  0er  6779  mapprc  6864  mapsnconst  6906  ixpf  6932  mptelixpg  6946  idssen  6993  ener  6996  en0  7012  en1  7016  en1bg  7017  2dom  7023  modom  7037  enm  7047  xpsnen  7048  ssenen  7080  snnen2og  7088  php5dom  7092  phpm  7095  findcard  7120  findcard2  7121  findcard2s  7122  unfiexmid  7153  fiintim  7166  fidcenumlemim  7194  sbthlem1  7199  fiss  7219  djuexb  7286  djuss  7312  eldju2ndl  7314  eldju2ndr  7315  ctssdclemr  7354  exmidlpo  7385  finnum  7430  ficardon  7436  exmidfodomrlemim  7455  acnrcl  7459  3nsssucpw1  7497  indpi  7605  subhalfnqq  7677  archnqq  7680  enq0sym  7695  nqnq0pi  7701  nqnq0  7704  mulnnnq0  7713  prml  7740  prmu  7741  prssnql  7742  prssnqu  7743  prcdnql  7747  prcunqu  7748  prltlu  7750  prnmaxl  7751  prnminu  7752  prloc  7754  prdisj  7755  addcanprg  7879  recexprlemopl  7888  recexprlemopu  7890  cauappcvgprlemladdfu  7917  caucvgprlemladdfu  7940  recexgt0sr  8036  renfdisj  8281  axsuploc  8294  negf1o  8603  recexre  8800  apsqgt0  8823  apreim  8825  aprcl  8868  recexaplem2  8874  rerecclap  8952  nn0ge0  9469  elnnnn0b  9488  xnn0xr  9514  xnn0nemnf  9520  xnn0nnn0pnf  9522  znegcl  9554  zeo  9629  nn0ind  9638  nn0ind-raph  9641  uzn0  9816  eluzaddi  9827  eluzsubi  9828  uznn0sub  9832  uz3m2nn  9851  uznnssnn  9855  uz2m1nn  9883  uz2mulcl  9886  indstr2  9887  qmulz  9901  qre  9903  qnegcl  9914  qreccl  9920  rphalflt  9962  nn0ledivnn  10046  xrltnr  10058  nltpnft  10093  ngtmnft  10096  xrrebnd  10098  xnegcl  10111  xnegneg  10112  xltnegi  10114  xrpnfdc  10121  xrmnfdc  10122  xnegid  10138  xaddid1  10141  xnn0lenn0nn0  10144  xnn0xadd0  10146  xposdif  10161  elioore  10191  elfzuz2  10309  uzsubsubfz  10327  fzdisj  10332  fzmmmeqm  10338  elfz0ubfz0  10405  elfz0fzfz0  10406  fz0fzelfz0  10407  fz0fzdiffz0  10410  elfzmlbp  10412  difelfzle  10414  difelfznle  10415  nn0disj  10418  2ffzeq  10421  fzo1fzo0n0  10468  elfzo0z  10469  elfzo0le  10470  fzonmapblen  10472  fzofzim  10473  elfzodifsumelfzo  10492  elfzonlteqm1  10501  fzonn0p1p1  10504  elfzom1p1elfzo  10505  ssfzo12bi  10516  ubmelm1fzo  10517  fzind2  10531  subfzo0  10534  infssuzcldc  10541  rebtwn2z  10560  fldiv4p1lem1div2  10611  fldiv4lem1div2  10613  flqeqceilz  10626  zmodidfzoimp  10662  modfzo0difsn  10703  nnsinds  10753  nn0sinds  10754  expcl2lemap  10859  qexpclz  10868  zzlesq  11016  facp1  11038  facnn2  11042  faclbnd3  11051  bcn1  11066  hashfz0  11135  wrdf  11168  swrdswrdlem  11334  swrdswrd  11335  swrdccatin1  11355  pfxccatin12lem2a  11357  pfxccatin12lem1  11358  swrdccatin2  11359  pfxccatin12lem2  11361  pfxccatin12lem3  11362  pfxccatin12  11363  pfxccat3  11364  swrdccat  11365  swrdccat3blem  11369  cvg1nlemres  11608  rexanuz  11611  fclim  11917  climmo  11921  iser3shft  11969  fsumsplitsn  12034  fsum2dlemstep  12058  fisumcom2  12062  arisum  12122  arisum2  12123  prodmodc  12202  fprodfac  12239  fprod2dlemstep  12246  fprodcom2fi  12250  fprodsplitsn  12257  eftlub  12314  ef01bndlem  12380  sin01gt0  12386  cos01gt0  12387  sin02gt0  12388  dvdsdivcl  12474  addmodlteqALT  12483  odd2np1  12497  oddge22np1  12505  m1expe  12523  nn0enne  12526  nn0o1gt2  12529  nno  12530  ndvdsadd  12555  dfgcd2  12648  mulgcd  12650  algfx  12687  prmind2  12755  prm2orodd  12761  prmgt1  12767  oddprmgt2  12769  dfphi2  12855  nnnn0modprm0  12891  prm23lt5  12899  pythagtriplem2  12902  pcz  12968  dvdsprmpweqnn  12972  oddprmdvds  12990  prmunb  12998  4sqlem4  13028  4sqlem19  13045  evenennn  13077  fngsum  13534  igsumvalx  13535  dfgrp3me  13746  mulgnn0gsum  13778  rngdi  14017  rngdir  14018  dvdsrcl2  14177  unitinvcl  14201  unitinvinv  14202  unitlinv  14204  unitrinv  14205  rmodislmodlem  14429  rmodislmod  14430  zrhval  14696  psrbagf  14749  distop  14879  ntrss  14913  ssntr  14916  lmrcl  14986  txuni2  15050  txcn  15069  hmeocnvb  15112  xmetunirn  15152  blssioo  15347  divcnap  15359  cdivcncfap  15398  dedekindeulemlub  15414  dedekindicclemlub  15423  dvexp2  15506  elply2  15529  plyco  15553  pilem3  15577  sincosq1sgn  15620  sincosq2sgn  15621  sincosq3sgn  15622  sincosq4sgn  15623  sinq12gt0  15624  fsumdvdsmul  15788  zabsle1  15801  lgsdir2lem4  15833  gausslemma2dlem0f  15856  gausslemma2dlem1a  15860  gausslemma2dlem2  15864  gausslemma2dlem3  15865  gausslemma2dlem4  15866  2lgslem1a1  15888  2lgslem3  15903  2lgsoddprmlem3  15913  2lgsoddprm  15915  2sqlem2  15917  2sqlem10  15927  vtxvalprc  15979  iedgvalprc  15980  upgrex  16027  umgredg  16069  ausgrusgrben  16092  usgruspgrben  16110  usgrislfuspgrdom  16114  uhgr2edg  16130  uspgredg2v  16145  griedg0ssusgr  16175  subusgr  16199  wlkv  16250  wlk1walkdom  16283  trlsv  16308  trlf1  16312  clwwlk1loop  16323  clwwlkext2edg  16346  umgr2cwwkdifex  16349  clwwlknonex2lem2  16362  clwwlknonex2e  16364  eupthv  16370  eupth2lem3lem4fi  16397  konigsberglem5  16416  bj-pm2.18st  16451  bj-dcstab  16457  decidi  16496  sumdc2  16500  bj-charfunbi  16510  bdel  16544  bdssex  16601  bj-indind  16631  findset  16644  nninfall  16718  trirec0  16759  neap0mkv  16785