Theorem sylbi 120

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 119	. 2 |- ( ph -> ps )
3		sylbi.2	. 2 |- ( ps -> ch )
4	2, 3	syl 14	1 |- ( ph -> ch )

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylbb  122  sylbb2  137  3imtr4i  200  simplbiim  385  mpan10  466  an12s  555  an32s  558  an4s  578  sylnbi  668  dcim  831  notnotrdc  833  condcOLD  844  pm2.61ddc  851  pm5.18dc  873  pm2.25dc  883  pm2.85dc  895  pm5.12dc  900  pm5.14dc  901  pm5.55dc  903  peircedc  904  pm5.54dc  908  dcor  925  pm5.62dc  935  pm5.63dc  936  pm4.83dc  941  3simpb  985  3simpc  986  3imp  1183  3com12  1197  3com13  1198  syl3anb  1271  xoranor  1367  xorbin  1374  xordc1  1383  biassdc  1385  nfr  1506  nfand  1556  19.21t  1570  19.30dc  1615  exintrbi  1621  19.9t  1630  nfnt  1644  equveli  1747  exdistrfor  1788  sbcof2  1798  sbidm  1839  sbi1v  1879  sbalyz  1987  sbal1yz  1989  nfsb4t  2002  euex  2044  eumo0  2045  mor  2056  exmodc  2064  mo3h  2067  mopick  2092  moexexdc  2098  euexex  2099  2euex  2101  exists2  2111  eqcoms  2168  eleq2s  2260  nfcr  2299  necon3ai  2384  rexnalim  2454  dfrex2dc  2456  rexex  2511  rsp  2512  ralim  2524  rexim  2559  r19.32r  2611  r19.44av  2624  r19.45av  2625  gencl  2757  gencbvex  2771  gencbval  2773  vtoclgf  2783  vtoclg1f  2784  pm13.183  2863  elrabi  2878  eueq2dc  2898  eueq3dc  2899  mob2  2905  euxfr2dc  2910  reu3  2915  rmoim  2926  2rmorex  2931  sbcex  2958  sbcbi2  3000  ra5  3038  sseq1  3164  difdif  3246  dfss4st  3354  difindiss  3375  undif3ss  3382  dfrab3ss  3399  abvor0dc  3431  reldisj  3459  disjel  3462  inssdif0im  3475  uneqdifeqim  3493  r19.2m  3494  r19.2mOLD  3495  r19.3rm  3496  r19.9rmv  3499  rexm  3507  ralm  3512  raaanlem  3513  ifnefalse  3530  ifnotdc  3555  ifandc  3556  ifmdc  3557  nelpri  3599  nelprd  3601  prprc1  3683  difprsn2  3712  diftpsn3  3713  snsssn  3740  preqr2  3748  preq12b  3749  opthpr  3751  prneimg  3753  oprcl  3781  pwprss  3784  intmin4  3851  uniintabim  3860  dfiin2g  3898  iinss2  3917  iundif2ss  3930  disjnim  3972  disjnims  3973  invdisj  3975  disjiun  3976  brne0  4030  brm  4031  trel  4086  trss  4088  ssex  4118  bnd2  4151  abssexg  4160  exmidexmid  4174  rext  4192  unipw  4194  euabex  4202  mss  4203  exss  4204  copsexg  4221  opelopabsb  4237  pwssunim  4261  epelg  4267  sowlin  4297  sotritric  4301  elsuci  4380  sucprc  4389  reusv3  4437  ordon  4462  onsucmin  4483  onsucelsucr  4484  unon  4487  onsucelsucexmid  4506  setind  4515  setind2  4516  sucprcreg  4525  en2lp  4530  eunex  4537  ordsoexmid  4538  ordpwsucss  4543  tfi  4558  peano1  4570  peano2  4571  find  4575  0nelelxp  4632  opelxp  4633  elvvuni  4667  optocl  4679  ralxpf  4749  rexxpf  4750  relop  4753  breldm  4807  dmxpm  4823  elreldm  4829  dmrnssfld  4866  dmcosseq  4874  resabs1  4912  resima2  4917  issref  4985  asymref  4988  xpidtr  4993  trin2  4994  poirr2  4995  xpmlem  5023  dmxpss  5033  xp11m  5041  cnveqb  5058  dfco2a  5103  cores2  5115  coi2  5119  relcnvtr  5122  relresfld  5132  relcnvexb  5142  cnviinm  5144  iotauni  5164  iota1  5166  iota4  5170  dffun8  5215  funcnvsn  5232  imadif  5267  imainlem  5268  fcoi1  5367  fcoi2  5368  f0rn0  5381  f1ocnv  5444  f1ocnvb  5445  fun11iun  5452  ffoss  5463  f1o00  5466  fo00  5467  relelfvdm  5517  nfvres  5518  nfunsn  5519  ssimaex  5546  fvmptss2  5560  fvmptssdm  5569  unpreima  5609  respreima  5612  elrnrexdm  5623  elrnrexdmb  5624  rexrnmpt  5627  dffo4  5632  rnmptss  5645  fvpr1  5688  fvpr2  5689  elunirn  5733  f1veqaeq  5736  isores1  5781  riotauni  5803  riotacl2  5810  riota1  5815  riota1a  5816  snriota  5826  eusvobj2  5827  acexmidlema  5832  acexmidlemb  5833  acexmidlem2  5838  oprabid  5870  0neqopab  5883  brabvv  5884  1stval2  6120  2ndval2  6121  xp1st  6130  xp2nd  6131  unielxp  6139  releldm2  6150  cnvf1o  6189  fo2ndf  6191  poxp  6196  reldmtpos  6217  dftpos4  6227  tpostpos  6228  tpostpos2  6229  iunon  6248  smoel  6264  tfrlem4  6277  tfrlem7  6281  tfrlem8  6282  tfrlem9  6283  nnaord  6473  ecexr  6502  swoord1  6526  swoord2  6527  0er  6531  mapprc  6614  mapsnconst  6656  ixpf  6682  mptelixpg  6696  idssen  6739  ener  6741  en0  6757  en1  6761  en1bg  6762  2dom  6767  enm  6782  xpsnen  6783  ssenen  6813  snnen2og  6821  php5dom  6825  phpm  6827  findcard  6850  findcard2  6851  findcard2s  6852  unfiexmid  6879  fiintim  6890  fidcenumlemim  6913  sbthlem1  6918  fiss  6938  djuexb  7005  djuss  7031  eldju2ndl  7033  eldju2ndr  7034  ctssdclemr  7073  exmidlpo  7103  finnum  7135  exmidfodomrlemim  7153  3nsssucpw1  7188  indpi  7279  subhalfnqq  7351  archnqq  7354  enq0sym  7369  nqnq0pi  7375  nqnq0  7378  mulnnnq0  7387  prml  7414  prmu  7415  prssnql  7416  prssnqu  7417  prcdnql  7421  prcunqu  7422  prltlu  7424  prnmaxl  7425  prnminu  7426  prloc  7428  prdisj  7429  addcanprg  7553  recexprlemopl  7562  recexprlemopu  7564  cauappcvgprlemladdfu  7591  caucvgprlemladdfu  7614  recexgt0sr  7710  renfdisj  7954  axsuploc  7967  negf1o  8276  recexre  8472  apsqgt0  8495  apreim  8497  aprcl  8540  recexaplem2  8545  rerecclap  8622  nn0ge0  9135  elnnnn0b  9154  xnn0xr  9178  xnn0nemnf  9184  xnn0nnn0pnf  9186  znegcl  9218  zeo  9292  nn0ind  9301  nn0ind-raph  9304  uzn0  9477  eluzaddi  9488  eluzsubi  9489  uznn0sub  9493  uz3m2nn  9507  uznnssnn  9511  uz2m1nn  9539  uz2mulcl  9542  indstr2  9543  qmulz  9557  qre  9559  qnegcl  9570  qreccl  9576  rphalflt  9615  nn0ledivnn  9699  xrltnr  9711  nltpnft  9746  ngtmnft  9749  xrrebnd  9751  xnegcl  9764  xnegneg  9765  xltnegi  9767  xrpnfdc  9774  xrmnfdc  9775  xnegid  9791  xaddid1  9794  xnn0lenn0nn0  9797  xnn0xadd0  9799  xposdif  9814  elioore  9844  elfzuz2  9960  uzsubsubfz  9978  fzdisj  9983  fzmmmeqm  9989  elfz0ubfz0  10056  elfz0fzfz0  10057  fz0fzelfz0  10058  fz0fzdiffz0  10061  elfzmlbp  10063  difelfzle  10065  difelfznle  10066  nn0disj  10069  2ffzeq  10072  fzo1fzo0n0  10114  elfzo0z  10115  elfzo0le  10116  fzonmapblen  10118  fzofzim  10119  elfzodifsumelfzo  10132  elfzonlteqm1  10141  fzonn0p1p1  10144  elfzom1p1elfzo  10145  ssfzo12bi  10156  ubmelm1fzo  10157  fzind2  10170  subfzo0  10173  rebtwn2z  10186  fldiv4p1lem1div2  10236  flqeqceilz  10249  zmodidfzoimp  10285  modfzo0difsn  10326  nnsinds  10374  nn0sinds  10375  expcl2lemap  10463  qexpclz  10472  facp1  10639  facnn2  10643  faclbnd3  10652  bcn1  10667  hashfz0  10734  cvg1nlemres  10923  rexanuz  10926  fclim  11231  climmo  11235  iser3shft  11283  fsumsplitsn  11347  fsum2dlemstep  11371  fisumcom2  11375  arisum  11435  arisum2  11436  prodmodc  11515  fprodfac  11552  fprod2dlemstep  11559  fprodcom2fi  11563  fprodsplitsn  11570  eftlub  11627  ef01bndlem  11693  sin01gt0  11698  cos01gt0  11699  sin02gt0  11700  dvdsdivcl  11784  addmodlteqALT  11793  odd2np1  11806  oddge22np1  11814  m1expe  11832  nn0enne  11835  nn0o1gt2  11838  nno  11839  ndvdsadd  11864  infssuzcldc  11880  dfgcd2  11943  mulgcd  11945  algfx  11980  prmind2  12048  prm2orodd  12054  prmgt1  12060  oddprmgt2  12062  dfphi2  12148  nnnn0modprm0  12183  prm23lt5  12191  pythagtriplem2  12194  pcz  12259  dvdsprmpweqnn  12263  oddprmdvds  12280  prmunb  12288  4sqlem4  12318  evenennn  12322  distop  12685  ntrss  12719  ssntr  12722  lmrcl  12791  lmreltop  12793  txuni2  12856  txcn  12875  hmeocnvb  12918  xmetunirn  12958  blssioo  13145  divcnap  13155  cdivcncfap  13187  dedekindeulemlub  13198  dedekindicclemlub  13207  dvexp2  13276  pilem3  13304  sincosq1sgn  13347  sincosq2sgn  13348  sincosq3sgn  13349  sincosq4sgn  13350  sinq12gt0  13351  zabsle1  13500  lgsdir2lem4  13532  2sqlem2  13551  2sqlem10  13561  bj-pm2.18st  13591  bj-dcstab  13597  decidi  13636  sumdc2  13640  bj-charfunbi  13653  bdel  13687  bdssex  13744  bj-indind  13774  findset  13787  nninfall  13849  trirec0  13883