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  471  an12s  560  an32s  563  an4s  583  sylnbi  673  dcim  836  notnotrdc  838  condcOLD  849  pm2.61ddc  856  pm5.18dc  878  pm2.25dc  888  pm2.85dc  900  pm5.12dc  905  pm5.14dc  906  pm5.55dc  908  peircedc  909  pm5.54dc  913  dcor  930  pm5.62dc  940  pm5.63dc  941  pm4.83dc  946  3simpb  990  3simpc  991  3imp  1188  3com12  1202  3com13  1203  syl3anb  1276  xoranor  1372  xorbin  1379  xordc1  1388  biassdc  1390  nfr  1511  nfand  1561  19.21t  1575  19.30dc  1620  exintrbi  1626  19.9t  1635  nfnt  1649  equveli  1752  exdistrfor  1793  sbcof2  1803  sbidm  1844  sbi1v  1884  sbalyz  1992  sbal1yz  1994  nfsb4t  2007  euex  2049  eumo0  2050  mor  2061  exmodc  2069  mo3h  2072  mopick  2097  moexexdc  2103  euexex  2104  2euex  2106  exists2  2116  eqcoms  2173  eleq2s  2265  nfcr  2304  necon3ai  2389  rexnalim  2459  dfrex2dc  2461  rexex  2516  rsp  2517  ralim  2529  rexim  2564  r19.32r  2616  r19.44av  2629  r19.45av  2630  gencl  2762  gencbvex  2776  gencbval  2778  vtoclgf  2788  vtoclg1f  2789  pm13.183  2868  elrabi  2883  eueq2dc  2903  eueq3dc  2904  mob2  2910  euxfr2dc  2915  reu3  2920  rmoim  2931  2rmorex  2936  sbcex  2963  sbcbi2  3005  ra5  3043  sseq1  3170  difdif  3252  dfss4st  3360  difindiss  3381  undif3ss  3388  dfrab3ss  3405  abvor0dc  3438  reldisj  3466  disjel  3469  inssdif0im  3482  uneqdifeqim  3500  r19.2m  3501  r19.2mOLD  3502  r19.3rm  3503  r19.9rmv  3506  rexm  3514  ralm  3519  raaanlem  3520  ifnefalse  3537  ifnotdc  3562  ifandc  3563  ifmdc  3565  nelpri  3607  nelprd  3609  prprc1  3691  difprsn2  3720  diftpsn3  3721  snsssn  3748  preqr2  3756  preq12b  3757  opthpr  3759  prneimg  3761  oprcl  3789  pwprss  3792  intmin4  3859  uniintabim  3868  dfiin2g  3906  iinss2  3925  iundif2ss  3938  disjnim  3980  disjnims  3981  invdisj  3983  disjiun  3984  brne0  4038  brm  4039  trel  4094  trss  4096  ssex  4126  bnd2  4159  abssexg  4168  exmidexmid  4182  rext  4200  unipw  4202  euabex  4210  mss  4211  exss  4212  copsexg  4229  opelopabsb  4245  pwssunim  4269  epelg  4275  sowlin  4305  sotritric  4309  elsuci  4388  sucprc  4397  reusv3  4445  ordon  4470  onsucmin  4491  onsucelsucr  4492  unon  4495  onsucelsucexmid  4514  setind  4523  setind2  4524  sucprcreg  4533  en2lp  4538  eunex  4545  ordsoexmid  4546  ordpwsucss  4551  tfi  4566  peano1  4578  peano2  4579  find  4583  0nelelxp  4640  opelxp  4641  elvvuni  4675  optocl  4687  ralxpf  4757  rexxpf  4758  relop  4761  breldm  4815  dmxpm  4831  elreldm  4837  dmrnssfld  4874  dmcosseq  4882  resabs1  4920  resima2  4925  issref  4993  asymref  4996  xpidtr  5001  trin2  5002  poirr2  5003  xpmlem  5031  dmxpss  5041  xp11m  5049  cnveqb  5066  dfco2a  5111  cores2  5123  coi2  5127  relcnvtr  5130  relresfld  5140  relcnvexb  5150  cnviinm  5152  iotauni  5172  iota1  5174  iota4  5178  iotam  5190  dffun8  5226  funcnvsn  5243  imadif  5278  imainlem  5279  fcoi1  5378  fcoi2  5379  f0rn0  5392  f1ocnv  5455  f1ocnvb  5456  fun11iun  5463  ffoss  5474  f1o00  5477  fo00  5478  relelfvdm  5528  nfvres  5529  nfunsn  5530  ssimaex  5557  fvmptss2  5571  fvmptssdm  5580  unpreima  5621  respreima  5624  elrnrexdm  5635  elrnrexdmb  5636  rexrnmpt  5639  dffo4  5644  rnmptss  5657  fvpr1  5700  fvpr2  5701  elunirn  5745  f1veqaeq  5748  isores1  5793  riotauni  5815  riotacl2  5822  riota1  5827  riota1a  5828  snriota  5838  eusvobj2  5839  acexmidlema  5844  acexmidlemb  5845  acexmidlem2  5850  oprabid  5885  0neqopab  5898  brabvv  5899  1stval2  6134  2ndval2  6135  xp1st  6144  xp2nd  6145  unielxp  6153  releldm2  6164  cnvf1o  6204  fo2ndf  6206  poxp  6211  reldmtpos  6232  dftpos4  6242  tpostpos  6243  tpostpos2  6244  iunon  6263  smoel  6279  tfrlem4  6292  tfrlem7  6296  tfrlem8  6297  tfrlem9  6298  nnaord  6488  ecexr  6518  swoord1  6542  swoord2  6543  0er  6547  mapprc  6630  mapsnconst  6672  ixpf  6698  mptelixpg  6712  idssen  6755  ener  6757  en0  6773  en1  6777  en1bg  6778  2dom  6783  enm  6798  xpsnen  6799  ssenen  6829  snnen2og  6837  php5dom  6841  phpm  6843  findcard  6866  findcard2  6867  findcard2s  6868  unfiexmid  6895  fiintim  6906  fidcenumlemim  6929  sbthlem1  6934  fiss  6954  djuexb  7021  djuss  7047  eldju2ndl  7049  eldju2ndr  7050  ctssdclemr  7089  exmidlpo  7119  finnum  7160  exmidfodomrlemim  7178  3nsssucpw1  7213  indpi  7304  subhalfnqq  7376  archnqq  7379  enq0sym  7394  nqnq0pi  7400  nqnq0  7403  mulnnnq0  7412  prml  7439  prmu  7440  prssnql  7441  prssnqu  7442  prcdnql  7446  prcunqu  7447  prltlu  7449  prnmaxl  7450  prnminu  7451  prloc  7453  prdisj  7454  addcanprg  7578  recexprlemopl  7587  recexprlemopu  7589  cauappcvgprlemladdfu  7616  caucvgprlemladdfu  7639  recexgt0sr  7735  renfdisj  7979  axsuploc  7992  negf1o  8301  recexre  8497  apsqgt0  8520  apreim  8522  aprcl  8565  recexaplem2  8570  rerecclap  8647  nn0ge0  9160  elnnnn0b  9179  xnn0xr  9203  xnn0nemnf  9209  xnn0nnn0pnf  9211  znegcl  9243  zeo  9317  nn0ind  9326  nn0ind-raph  9329  uzn0  9502  eluzaddi  9513  eluzsubi  9514  uznn0sub  9518  uz3m2nn  9532  uznnssnn  9536  uz2m1nn  9564  uz2mulcl  9567  indstr2  9568  qmulz  9582  qre  9584  qnegcl  9595  qreccl  9601  rphalflt  9640  nn0ledivnn  9724  xrltnr  9736  nltpnft  9771  ngtmnft  9774  xrrebnd  9776  xnegcl  9789  xnegneg  9790  xltnegi  9792  xrpnfdc  9799  xrmnfdc  9800  xnegid  9816  xaddid1  9819  xnn0lenn0nn0  9822  xnn0xadd0  9824  xposdif  9839  elioore  9869  elfzuz2  9985  uzsubsubfz  10003  fzdisj  10008  fzmmmeqm  10014  elfz0ubfz0  10081  elfz0fzfz0  10082  fz0fzelfz0  10083  fz0fzdiffz0  10086  elfzmlbp  10088  difelfzle  10090  difelfznle  10091  nn0disj  10094  2ffzeq  10097  fzo1fzo0n0  10139  elfzo0z  10140  elfzo0le  10141  fzonmapblen  10143  fzofzim  10144  elfzodifsumelfzo  10157  elfzonlteqm1  10166  fzonn0p1p1  10169  elfzom1p1elfzo  10170  ssfzo12bi  10181  ubmelm1fzo  10182  fzind2  10195  subfzo0  10198  rebtwn2z  10211  fldiv4p1lem1div2  10261  flqeqceilz  10274  zmodidfzoimp  10310  modfzo0difsn  10351  nnsinds  10399  nn0sinds  10400  expcl2lemap  10488  qexpclz  10497  facp1  10664  facnn2  10668  faclbnd3  10677  bcn1  10692  hashfz0  10760  cvg1nlemres  10949  rexanuz  10952  fclim  11257  climmo  11261  iser3shft  11309  fsumsplitsn  11373  fsum2dlemstep  11397  fisumcom2  11401  arisum  11461  arisum2  11462  prodmodc  11541  fprodfac  11578  fprod2dlemstep  11585  fprodcom2fi  11589  fprodsplitsn  11596  eftlub  11653  ef01bndlem  11719  sin01gt0  11724  cos01gt0  11725  sin02gt0  11726  dvdsdivcl  11810  addmodlteqALT  11819  odd2np1  11832  oddge22np1  11840  m1expe  11858  nn0enne  11861  nn0o1gt2  11864  nno  11865  ndvdsadd  11890  infssuzcldc  11906  dfgcd2  11969  mulgcd  11971  algfx  12006  prmind2  12074  prm2orodd  12080  prmgt1  12086  oddprmgt2  12088  dfphi2  12174  nnnn0modprm0  12209  prm23lt5  12217  pythagtriplem2  12220  pcz  12285  dvdsprmpweqnn  12289  oddprmdvds  12306  prmunb  12314  4sqlem4  12344  evenennn  12348  distop  12879  ntrss  12913  ssntr  12916  lmrcl  12985  lmreltop  12987  txuni2  13050  txcn  13069  hmeocnvb  13112  xmetunirn  13152  blssioo  13339  divcnap  13349  cdivcncfap  13381  dedekindeulemlub  13392  dedekindicclemlub  13401  dvexp2  13470  pilem3  13498  sincosq1sgn  13541  sincosq2sgn  13542  sincosq3sgn  13543  sincosq4sgn  13544  sinq12gt0  13545  zabsle1  13694  lgsdir2lem4  13726  2sqlem2  13745  2sqlem10  13755  bj-pm2.18st  13785  bj-dcstab  13791  decidi  13830  sumdc2  13834  bj-charfunbi  13846  bdel  13880  bdssex  13937  bj-indind  13967  findset  13980  nninfall  14042  trirec0  14076