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  588  sylnbi  679  dcim  842  notnotrdc  844  condcOLD  855  pm2.61ddc  862  pm5.18dc  884  pm2.25dc  894  pm2.85dc  906  pm5.12dc  911  pm5.14dc  912  pm5.55dc  914  peircedc  915  pm5.54dc  919  dcand  934  dcor  937  pm5.62dc  947  pm5.63dc  948  pm4.83dc  953  3simpb  997  3simpc  998  3imp  1195  3com12  1209  3com13  1210  syl3anb  1292  xoranor  1388  xorbin  1395  xordc1  1404  biassdc  1406  nfr  1532  nfand  1582  19.21t  1596  19.30dc  1641  exintrbi  1647  19.9t  1656  nfnt  1670  equveli  1773  exdistrfor  1814  sbcof2  1824  sbidm  1865  sbi1v  1906  sbalyz  2018  sbal1yz  2020  nfsb4t  2033  euex  2075  eumo0  2076  mor  2087  exmodc  2095  mo3h  2098  mopick  2123  moexexdc  2129  euexex  2130  2euex  2132  exists2  2142  eqcoms  2199  eleq2s  2291  nfcr  2331  necon3ai  2416  rexnalim  2486  dfrex2dc  2488  rexex  2543  rsp  2544  ralim  2556  rexim  2591  r19.32r  2643  r19.44av  2656  r19.45av  2657  gencl  2795  gencbvex  2810  gencbval  2812  vtoclgf  2822  vtoclg1f  2823  pm13.183  2902  elrabi  2917  eueq2dc  2937  eueq3dc  2938  mob2  2944  euxfr2dc  2949  reu3  2954  rmoim  2965  2rmorex  2970  sbcex  2998  sbcbi2  3040  ra5  3078  sseq1  3206  difdif  3288  dfss4st  3396  difindiss  3417  undif3ss  3424  dfrab3ss  3441  abvor0dc  3474  reldisj  3502  disjel  3505  inssdif0im  3518  uneqdifeqim  3536  r19.2m  3537  r19.2mOLD  3538  r19.3rm  3539  r19.9rmv  3542  rexm  3550  ralm  3554  raaanlem  3555  ifnefalse  3572  ifnotdc  3598  ifandc  3599  ifmdc  3601  nelpri  3646  nelprd  3648  prprc1  3730  difprsn2  3762  diftpsn3  3763  snsssn  3791  preqr2  3799  preq12b  3800  opthpr  3802  prneimg  3804  oprcl  3832  pwprss  3835  intmin4  3902  uniintabim  3911  dfiin2g  3949  iinss2  3969  iundif2ss  3982  disjnim  4024  disjnims  4025  invdisj  4027  disjiun  4028  brne0  4082  brm  4083  trel  4138  trss  4140  ssex  4170  bnd2  4206  abssexg  4215  exmidexmid  4229  rext  4248  unipw  4250  euabex  4258  mss  4259  exss  4260  copsexg  4277  opelopabsb  4294  pwssunim  4319  epelg  4325  sowlin  4355  sotritric  4359  elsuci  4438  sucprc  4447  reusv3  4495  ordon  4522  onsucmin  4543  onsucelsucr  4544  unon  4547  onsucelsucexmid  4566  setind  4575  setind2  4576  sucprcreg  4585  en2lp  4590  eunex  4597  ordsoexmid  4598  ordpwsucss  4603  tfi  4618  peano1  4630  peano2  4631  find  4635  0nelelxp  4692  opelxp  4693  elvvuni  4727  optocl  4739  ralxpf  4812  rexxpf  4813  relop  4816  breldm  4870  dmxpm  4886  elreldm  4892  dmrnssfld  4929  dmcosseq  4937  resabs1  4975  resima2  4980  issref  5052  asymref  5055  xpidtr  5060  trin2  5061  poirr2  5062  xpmlem  5090  dmxpss  5100  xp11m  5108  cnveqb  5125  dfco2a  5170  cores2  5182  coi2  5186  relcnvtr  5189  relresfld  5199  relcnvexb  5209  cnviinm  5211  iotauni  5231  iota1  5233  iota4  5238  iotam  5250  dffun8  5286  funcnvsn  5303  imadif  5338  imainlem  5339  fcoi1  5438  fcoi2  5439  f0rn0  5452  f1ocnv  5517  f1ocnvb  5518  fun11iun  5525  ffoss  5536  f1o00  5539  fo00  5540  relelfvdm  5590  nfvres  5592  nfunsn  5593  ssimaex  5622  fvmptss2  5636  fvmptssdm  5646  unpreima  5687  respreima  5690  elrnrexdm  5701  elrnrexdmb  5702  rexrnmpt  5705  dffo4  5710  rnmptss  5723  fvpr1  5766  fvpr2  5767  elunirn  5813  f1veqaeq  5816  isores1  5861  iotaexel  5882  riotauni  5884  riotacl2  5891  riota1  5896  riota1a  5897  snriota  5907  eusvobj2  5908  acexmidlema  5913  acexmidlemb  5914  acexmidlem2  5919  oprabid  5954  0neqopab  5967  brabvv  5968  1stval2  6213  2ndval2  6214  xp1st  6223  xp2nd  6224  unielxp  6232  releldm2  6243  cnvf1o  6283  fo2ndf  6285  poxp  6290  reldmtpos  6311  dftpos4  6321  tpostpos  6322  tpostpos2  6323  iunon  6342  smoel  6358  tfrlem4  6371  tfrlem7  6375  tfrlem8  6376  tfrlem9  6377  nnaord  6567  ecexr  6597  swoord1  6621  swoord2  6622  0er  6626  mapprc  6711  mapsnconst  6753  ixpf  6779  mptelixpg  6793  idssen  6836  ener  6838  en0  6854  en1  6858  en1bg  6859  2dom  6864  enm  6879  xpsnen  6880  ssenen  6912  snnen2og  6920  php5dom  6924  phpm  6926  findcard  6949  findcard2  6950  findcard2s  6951  unfiexmid  6979  fiintim  6992  fidcenumlemim  7018  sbthlem1  7023  fiss  7043  djuexb  7110  djuss  7136  eldju2ndl  7138  eldju2ndr  7139  ctssdclemr  7178  exmidlpo  7209  finnum  7250  exmidfodomrlemim  7268  3nsssucpw1  7303  indpi  7409  subhalfnqq  7481  archnqq  7484  enq0sym  7499  nqnq0pi  7505  nqnq0  7508  mulnnnq0  7517  prml  7544  prmu  7545  prssnql  7546  prssnqu  7547  prcdnql  7551  prcunqu  7552  prltlu  7554  prnmaxl  7555  prnminu  7556  prloc  7558  prdisj  7559  addcanprg  7683  recexprlemopl  7692  recexprlemopu  7694  cauappcvgprlemladdfu  7721  caucvgprlemladdfu  7744  recexgt0sr  7840  renfdisj  8086  axsuploc  8099  negf1o  8408  recexre  8605  apsqgt0  8628  apreim  8630  aprcl  8673  recexaplem2  8679  rerecclap  8757  nn0ge0  9274  elnnnn0b  9293  xnn0xr  9317  xnn0nemnf  9323  xnn0nnn0pnf  9325  znegcl  9357  zeo  9431  nn0ind  9440  nn0ind-raph  9443  uzn0  9617  eluzaddi  9628  eluzsubi  9629  uznn0sub  9633  uz3m2nn  9647  uznnssnn  9651  uz2m1nn  9679  uz2mulcl  9682  indstr2  9683  qmulz  9697  qre  9699  qnegcl  9710  qreccl  9716  rphalflt  9758  nn0ledivnn  9842  xrltnr  9854  nltpnft  9889  ngtmnft  9892  xrrebnd  9894  xnegcl  9907  xnegneg  9908  xltnegi  9910  xrpnfdc  9917  xrmnfdc  9918  xnegid  9934  xaddid1  9937  xnn0lenn0nn0  9940  xnn0xadd0  9942  xposdif  9957  elioore  9987  elfzuz2  10104  uzsubsubfz  10122  fzdisj  10127  fzmmmeqm  10133  elfz0ubfz0  10200  elfz0fzfz0  10201  fz0fzelfz0  10202  fz0fzdiffz0  10205  elfzmlbp  10207  difelfzle  10209  difelfznle  10210  nn0disj  10213  2ffzeq  10216  fzo1fzo0n0  10259  elfzo0z  10260  elfzo0le  10261  fzonmapblen  10263  fzofzim  10264  elfzodifsumelfzo  10277  elfzonlteqm1  10286  fzonn0p1p1  10289  elfzom1p1elfzo  10290  ssfzo12bi  10301  ubmelm1fzo  10302  fzind2  10315  subfzo0  10318  infssuzcldc  10325  rebtwn2z  10344  fldiv4p1lem1div2  10395  fldiv4lem1div2  10397  flqeqceilz  10410  zmodidfzoimp  10446  modfzo0difsn  10487  nnsinds  10537  nn0sinds  10538  expcl2lemap  10643  qexpclz  10652  zzlesq  10800  facp1  10822  facnn2  10826  faclbnd3  10835  bcn1  10850  hashfz0  10917  wrdf  10941  cvg1nlemres  11150  rexanuz  11153  fclim  11459  climmo  11463  iser3shft  11511  fsumsplitsn  11575  fsum2dlemstep  11599  fisumcom2  11603  arisum  11663  arisum2  11664  prodmodc  11743  fprodfac  11780  fprod2dlemstep  11787  fprodcom2fi  11791  fprodsplitsn  11798  eftlub  11855  ef01bndlem  11921  sin01gt0  11927  cos01gt0  11928  sin02gt0  11929  dvdsdivcl  12015  addmodlteqALT  12024  odd2np1  12038  oddge22np1  12046  m1expe  12064  nn0enne  12067  nn0o1gt2  12070  nno  12071  ndvdsadd  12096  dfgcd2  12181  mulgcd  12183  algfx  12220  prmind2  12288  prm2orodd  12294  prmgt1  12300  oddprmgt2  12302  dfphi2  12388  nnnn0modprm0  12424  prm23lt5  12432  pythagtriplem2  12435  pcz  12501  dvdsprmpweqnn  12505  oddprmdvds  12523  prmunb  12531  4sqlem4  12561  4sqlem19  12578  evenennn  12610  fngsum  13031  igsumvalx  13032  dfgrp3me  13232  mulgnn0gsum  13258  rngdi  13496  rngdir  13497  dvdsrcl2  13655  unitinvcl  13679  unitinvinv  13680  unitlinv  13682  unitrinv  13683  rmodislmodlem  13906  rmodislmod  13907  zrhval  14173  psrbagf  14224  distop  14321  ntrss  14355  ssntr  14358  lmrcl  14427  lmreltop  14429  txuni2  14492  txcn  14511  hmeocnvb  14554  xmetunirn  14594  blssioo  14789  divcnap  14801  cdivcncfap  14840  dedekindeulemlub  14856  dedekindicclemlub  14865  dvexp2  14948  elply2  14971  plyco  14995  pilem3  15019  sincosq1sgn  15062  sincosq2sgn  15063  sincosq3sgn  15064  sincosq4sgn  15065  sinq12gt0  15066  fsumdvdsmul  15227  zabsle1  15240  lgsdir2lem4  15272  gausslemma2dlem0f  15295  gausslemma2dlem1a  15299  gausslemma2dlem2  15303  gausslemma2dlem3  15304  gausslemma2dlem4  15305  2lgslem1a1  15327  2lgslem3  15342  2lgsoddprmlem3  15352  2lgsoddprm  15354  2sqlem2  15356  2sqlem10  15366  bj-pm2.18st  15396  bj-dcstab  15402  decidi  15441  sumdc2  15445  bj-charfunbi  15457  bdel  15491  bdssex  15548  bj-indind  15578  findset  15591  nninfall  15653  trirec0  15688  neap0mkv  15713