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  565  an32s  568  an4s  590  sylnbi  682  dcim  846  notnotrdc  848  condcOLD  859  pm2.61ddc  866  pm5.18dc  888  pm2.25dc  898  pm2.85dc  910  pm5.12dc  915  pm5.14dc  916  pm5.55dc  918  peircedc  919  pm5.54dc  923  dcand  938  dcor  941  pm5.62dc  951  pm5.63dc  952  pm4.83dc  957  ifp2  986  ifpor  993  1fpid3  1000  3simpb  1019  3simpc  1020  3imp  1217  3com12  1231  3com13  1232  syl3anb  1314  xoranor  1419  xorbin  1426  xordc1  1435  biassdc  1437  nfr  1564  nfand  1614  19.21t  1628  19.30dc  1673  exintrbi  1679  19.9t  1688  nfnt  1702  equveli  1805  exdistrfor  1846  sbcof2  1856  sbidm  1897  sbi1v  1938  sbalyz  2050  sbal1yz  2052  nfsb4t  2065  euex  2107  eumo0  2108  mor  2120  exmodc  2128  mo3h  2131  mopick  2156  moexexdc  2162  euexex  2163  2euex  2165  exists2  2175  eqcoms  2232  eleq2s  2324  nfcr  2364  necon3ai  2449  rexnalim  2519  dfrex2dc  2521  rexex  2576  rsp  2577  ralim  2589  rexim  2624  r19.32r  2677  r19.44av  2690  r19.45av  2691  gencl  2832  gencbvex  2847  gencbval  2849  vtoclgf  2859  vtoclg1f  2860  pm13.183  2941  elrabi  2956  eueq2dc  2976  eueq3dc  2977  mob2  2983  euxfr2dc  2988  reu3  2993  rmoim  3004  2rmorex  3009  sbcex  3037  sbcbi2  3079  ra5  3118  sseq1  3247  difdif  3329  dfss4st  3437  difindiss  3458  undif3ss  3465  dfrab3ss  3482  abvor0dc  3515  reldisj  3543  disjel  3546  inssdif0im  3559  uneqdifeqim  3577  r19.2m  3578  r19.2mOLD  3579  r19.3rm  3580  r19.9rmv  3583  rexm  3591  ralm  3595  raaanlem  3596  ifnefalse  3613  ifnotdc  3641  ifandc  3643  ifmdc  3645  nelpri  3690  nelprd  3692  prprc1  3775  difprsn2  3808  diftpsn3  3809  snsssn  3839  preqr2  3847  preq12b  3848  opthpr  3850  prneimg  3852  oprcl  3881  pwprss  3884  intmin4  3951  uniintabim  3960  dfiin2g  3998  iinss2  4018  iundif2ss  4031  disjnim  4073  disjnims  4074  invdisj  4076  disjiun  4078  brne0  4133  brm  4134  trel  4189  trss  4191  ssex  4221  bnd2  4257  abssexg  4266  exmidexmid  4280  rext  4301  unipw  4303  euabex  4311  mss  4312  exss  4313  copsexg  4330  opelopabsb  4348  pwssunim  4375  epelg  4381  sowlin  4411  sotritric  4415  elsuci  4494  sucprc  4503  reusv3  4551  ordon  4578  onsucmin  4599  onsucelsucr  4600  unon  4603  onsucelsucexmid  4622  setind  4631  setind2  4632  sucprcreg  4641  en2lp  4646  eunex  4653  ordsoexmid  4654  ordpwsucss  4659  tfi  4674  peano1  4686  peano2  4687  find  4691  0nelelxp  4748  opelxp  4749  elvvuni  4783  optocl  4795  ralxpf  4868  rexxpf  4869  relop  4872  breldm  4927  reldmm  4942  dmxpm  4944  elreldm  4950  dmrnssfld  4987  dmcosseq  4996  resabs1  5034  resima2  5039  issref  5111  asymref  5114  xpidtr  5119  trin2  5120  poirr2  5121  xpmlem  5149  dmxpss  5159  xp11m  5167  cnveqb  5184  dfco2a  5229  cores2  5241  coi2  5245  relcnvtr  5248  relresfld  5258  relcnvexb  5268  cnviinm  5270  iotauni  5291  iota1  5293  iota4  5298  iotam  5310  dffun8  5346  fununfun  5364  funcnvsn  5366  imadif  5401  imainlem  5402  fcoi1  5506  fcoi2  5507  f0rn0  5520  f1ocnv  5585  f1ocnvb  5586  fun11iun  5593  ffoss  5604  f1o00  5608  fo00  5609  relelfvdm  5659  nfvres  5663  nfunsn  5664  ssimaex  5695  fvmptss2  5709  fvmptssdm  5719  unpreima  5760  respreima  5763  elrnrexdm  5774  elrnrexdmb  5775  rexrnmpt  5778  dffo4  5783  rnmptss  5796  funiun  5816  funopdmsn  5819  fvpr1  5843  fvpr2  5844  elunirn  5890  f1veqaeq  5893  isores1  5938  iotaexel  5959  riotauni  5961  riotacl2  5969  riota1  5974  riota1a  5975  snriota  5986  eusvobj2  5987  acexmidlema  5992  acexmidlemb  5993  acexmidlem2  5998  oprabid  6033  0neqopab  6049  brabvv  6050  1stval2  6301  2ndval2  6302  xp1st  6311  xp2nd  6312  unielxp  6320  releldm2  6331  cnvf1o  6371  fo2ndf  6373  poxp  6378  reldmtpos  6399  dftpos4  6409  tpostpos  6410  tpostpos2  6411  iunon  6430  smoel  6446  tfrlem4  6459  tfrlem7  6463  tfrlem8  6464  tfrlem9  6465  nnaord  6655  ecexr  6685  swoord1  6709  swoord2  6710  0er  6714  mapprc  6799  mapsnconst  6841  ixpf  6867  mptelixpg  6881  idssen  6928  ener  6931  en0  6947  en1  6951  en1bg  6952  2dom  6958  enm  6979  xpsnen  6980  ssenen  7012  snnen2og  7020  php5dom  7024  phpm  7027  findcard  7050  findcard2  7051  findcard2s  7052  unfiexmid  7080  fiintim  7093  fidcenumlemim  7119  sbthlem1  7124  fiss  7144  djuexb  7211  djuss  7237  eldju2ndl  7239  eldju2ndr  7240  ctssdclemr  7279  exmidlpo  7310  finnum  7355  ficardon  7361  exmidfodomrlemim  7379  acnrcl  7383  3nsssucpw1  7421  indpi  7529  subhalfnqq  7601  archnqq  7604  enq0sym  7619  nqnq0pi  7625  nqnq0  7628  mulnnnq0  7637  prml  7664  prmu  7665  prssnql  7666  prssnqu  7667  prcdnql  7671  prcunqu  7672  prltlu  7674  prnmaxl  7675  prnminu  7676  prloc  7678  prdisj  7679  addcanprg  7803  recexprlemopl  7812  recexprlemopu  7814  cauappcvgprlemladdfu  7841  caucvgprlemladdfu  7864  recexgt0sr  7960  renfdisj  8206  axsuploc  8219  negf1o  8528  recexre  8725  apsqgt0  8748  apreim  8750  aprcl  8793  recexaplem2  8799  rerecclap  8877  nn0ge0  9394  elnnnn0b  9413  xnn0xr  9437  xnn0nemnf  9443  xnn0nnn0pnf  9445  znegcl  9477  zeo  9552  nn0ind  9561  nn0ind-raph  9564  uzn0  9738  eluzaddi  9749  eluzsubi  9750  uznn0sub  9754  uz3m2nn  9768  uznnssnn  9772  uz2m1nn  9800  uz2mulcl  9803  indstr2  9804  qmulz  9818  qre  9820  qnegcl  9831  qreccl  9837  rphalflt  9879  nn0ledivnn  9963  xrltnr  9975  nltpnft  10010  ngtmnft  10013  xrrebnd  10015  xnegcl  10028  xnegneg  10029  xltnegi  10031  xrpnfdc  10038  xrmnfdc  10039  xnegid  10055  xaddid1  10058  xnn0lenn0nn0  10061  xnn0xadd0  10063  xposdif  10078  elioore  10108  elfzuz2  10225  uzsubsubfz  10243  fzdisj  10248  fzmmmeqm  10254  elfz0ubfz0  10321  elfz0fzfz0  10322  fz0fzelfz0  10323  fz0fzdiffz0  10326  elfzmlbp  10328  difelfzle  10330  difelfznle  10331  nn0disj  10334  2ffzeq  10337  fzo1fzo0n0  10383  elfzo0z  10384  elfzo0le  10385  fzonmapblen  10387  fzofzim  10388  elfzodifsumelfzo  10407  elfzonlteqm1  10416  fzonn0p1p1  10419  elfzom1p1elfzo  10420  ssfzo12bi  10431  ubmelm1fzo  10432  fzind2  10445  subfzo0  10448  infssuzcldc  10455  rebtwn2z  10474  fldiv4p1lem1div2  10525  fldiv4lem1div2  10527  flqeqceilz  10540  zmodidfzoimp  10576  modfzo0difsn  10617  nnsinds  10667  nn0sinds  10668  expcl2lemap  10773  qexpclz  10782  zzlesq  10930  facp1  10952  facnn2  10956  faclbnd3  10965  bcn1  10980  hashfz0  11047  wrdf  11077  swrdswrdlem  11236  swrdswrd  11237  swrdccatin1  11257  pfxccatin12lem2a  11259  pfxccatin12lem1  11260  swrdccatin2  11261  pfxccatin12lem2  11263  pfxccatin12lem3  11264  pfxccatin12  11265  pfxccat3  11266  swrdccat  11267  swrdccat3blem  11271  cvg1nlemres  11496  rexanuz  11499  fclim  11805  climmo  11809  iser3shft  11857  fsumsplitsn  11921  fsum2dlemstep  11945  fisumcom2  11949  arisum  12009  arisum2  12010  prodmodc  12089  fprodfac  12126  fprod2dlemstep  12133  fprodcom2fi  12137  fprodsplitsn  12144  eftlub  12201  ef01bndlem  12267  sin01gt0  12273  cos01gt0  12274  sin02gt0  12275  dvdsdivcl  12361  addmodlteqALT  12370  odd2np1  12384  oddge22np1  12392  m1expe  12410  nn0enne  12413  nn0o1gt2  12416  nno  12417  ndvdsadd  12442  dfgcd2  12535  mulgcd  12537  algfx  12574  prmind2  12642  prm2orodd  12648  prmgt1  12654  oddprmgt2  12656  dfphi2  12742  nnnn0modprm0  12778  prm23lt5  12786  pythagtriplem2  12789  pcz  12855  dvdsprmpweqnn  12859  oddprmdvds  12877  prmunb  12885  4sqlem4  12915  4sqlem19  12932  evenennn  12964  fngsum  13421  igsumvalx  13422  dfgrp3me  13633  mulgnn0gsum  13665  rngdi  13903  rngdir  13904  dvdsrcl2  14063  unitinvcl  14087  unitinvinv  14088  unitlinv  14090  unitrinv  14091  rmodislmodlem  14314  rmodislmod  14315  zrhval  14581  psrbagf  14634  distop  14759  ntrss  14793  ssntr  14796  lmrcl  14866  txuni2  14930  txcn  14949  hmeocnvb  14992  xmetunirn  15032  blssioo  15227  divcnap  15239  cdivcncfap  15278  dedekindeulemlub  15294  dedekindicclemlub  15303  dvexp2  15386  elply2  15409  plyco  15433  pilem3  15457  sincosq1sgn  15500  sincosq2sgn  15501  sincosq3sgn  15502  sincosq4sgn  15503  sinq12gt0  15504  fsumdvdsmul  15665  zabsle1  15678  lgsdir2lem4  15710  gausslemma2dlem0f  15733  gausslemma2dlem1a  15737  gausslemma2dlem2  15741  gausslemma2dlem3  15742  gausslemma2dlem4  15743  2lgslem1a1  15765  2lgslem3  15780  2lgsoddprmlem3  15790  2lgsoddprm  15792  2sqlem2  15794  2sqlem10  15804  vtxvalprc  15856  iedgvalprc  15857  upgrex  15903  umgredg  15943  ausgrusgrben  15966  usgruspgrben  15984  usgrislfuspgrdom  15988  uhgr2edg  16004  uspgredg2v  16019  wlkv  16038  wlk1walkdom  16070  bj-pm2.18st  16114  bj-dcstab  16120  decidi  16159  sumdc2  16163  bj-charfunbi  16174  bdel  16208  bdssex  16265  bj-indind  16295  findset  16308  nninfall  16375  trirec0  16412  neap0mkv  16437