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  3437  reldisj  3465  disjel  3468  inssdif0im  3481  uneqdifeqim  3499  r19.2m  3500  r19.2mOLD  3501  r19.3rm  3502  r19.9rmv  3505  rexm  3513  ralm  3518  raaanlem  3519  ifnefalse  3536  ifnotdc  3561  ifandc  3562  ifmdc  3563  nelpri  3605  nelprd  3607  prprc1  3689  difprsn2  3718  diftpsn3  3719  snsssn  3746  preqr2  3754  preq12b  3755  opthpr  3757  prneimg  3759  oprcl  3787  pwprss  3790  intmin4  3857  uniintabim  3866  dfiin2g  3904  iinss2  3923  iundif2ss  3936  disjnim  3978  disjnims  3979  invdisj  3981  disjiun  3982  brne0  4036  brm  4037  trel  4092  trss  4094  ssex  4124  bnd2  4157  abssexg  4166  exmidexmid  4180  rext  4198  unipw  4200  euabex  4208  mss  4209  exss  4210  copsexg  4227  opelopabsb  4243  pwssunim  4267  epelg  4273  sowlin  4303  sotritric  4307  elsuci  4386  sucprc  4395  reusv3  4443  ordon  4468  onsucmin  4489  onsucelsucr  4490  unon  4493  onsucelsucexmid  4512  setind  4521  setind2  4522  sucprcreg  4531  en2lp  4536  eunex  4543  ordsoexmid  4544  ordpwsucss  4549  tfi  4564  peano1  4576  peano2  4577  find  4581  0nelelxp  4638  opelxp  4639  elvvuni  4673  optocl  4685  ralxpf  4755  rexxpf  4756  relop  4759  breldm  4813  dmxpm  4829  elreldm  4835  dmrnssfld  4872  dmcosseq  4880  resabs1  4918  resima2  4923  issref  4991  asymref  4994  xpidtr  4999  trin2  5000  poirr2  5001  xpmlem  5029  dmxpss  5039  xp11m  5047  cnveqb  5064  dfco2a  5109  cores2  5121  coi2  5125  relcnvtr  5128  relresfld  5138  relcnvexb  5148  cnviinm  5150  iotauni  5170  iota1  5172  iota4  5176  iotam  5188  dffun8  5224  funcnvsn  5241  imadif  5276  imainlem  5277  fcoi1  5376  fcoi2  5377  f0rn0  5390  f1ocnv  5453  f1ocnvb  5454  fun11iun  5461  ffoss  5472  f1o00  5475  fo00  5476  relelfvdm  5526  nfvres  5527  nfunsn  5528  ssimaex  5555  fvmptss2  5569  fvmptssdm  5578  unpreima  5618  respreima  5621  elrnrexdm  5632  elrnrexdmb  5633  rexrnmpt  5636  dffo4  5641  rnmptss  5654  fvpr1  5697  fvpr2  5698  elunirn  5742  f1veqaeq  5745  isores1  5790  riotauni  5812  riotacl2  5819  riota1  5824  riota1a  5825  snriota  5835  eusvobj2  5836  acexmidlema  5841  acexmidlemb  5842  acexmidlem2  5847  oprabid  5882  0neqopab  5895  brabvv  5896  1stval2  6131  2ndval2  6132  xp1st  6141  xp2nd  6142  unielxp  6150  releldm2  6161  cnvf1o  6201  fo2ndf  6203  poxp  6208  reldmtpos  6229  dftpos4  6239  tpostpos  6240  tpostpos2  6241  iunon  6260  smoel  6276  tfrlem4  6289  tfrlem7  6293  tfrlem8  6294  tfrlem9  6295  nnaord  6485  ecexr  6514  swoord1  6538  swoord2  6539  0er  6543  mapprc  6626  mapsnconst  6668  ixpf  6694  mptelixpg  6708  idssen  6751  ener  6753  en0  6769  en1  6773  en1bg  6774  2dom  6779  enm  6794  xpsnen  6795  ssenen  6825  snnen2og  6833  php5dom  6837  phpm  6839  findcard  6862  findcard2  6863  findcard2s  6864  unfiexmid  6891  fiintim  6902  fidcenumlemim  6925  sbthlem1  6930  fiss  6950  djuexb  7017  djuss  7043  eldju2ndl  7045  eldju2ndr  7046  ctssdclemr  7085  exmidlpo  7115  finnum  7147  exmidfodomrlemim  7165  3nsssucpw1  7200  indpi  7291  subhalfnqq  7363  archnqq  7366  enq0sym  7381  nqnq0pi  7387  nqnq0  7390  mulnnnq0  7399  prml  7426  prmu  7427  prssnql  7428  prssnqu  7429  prcdnql  7433  prcunqu  7434  prltlu  7436  prnmaxl  7437  prnminu  7438  prloc  7440  prdisj  7441  addcanprg  7565  recexprlemopl  7574  recexprlemopu  7576  cauappcvgprlemladdfu  7603  caucvgprlemladdfu  7626  recexgt0sr  7722  renfdisj  7966  axsuploc  7979  negf1o  8288  recexre  8484  apsqgt0  8507  apreim  8509  aprcl  8552  recexaplem2  8557  rerecclap  8634  nn0ge0  9147  elnnnn0b  9166  xnn0xr  9190  xnn0nemnf  9196  xnn0nnn0pnf  9198  znegcl  9230  zeo  9304  nn0ind  9313  nn0ind-raph  9316  uzn0  9489  eluzaddi  9500  eluzsubi  9501  uznn0sub  9505  uz3m2nn  9519  uznnssnn  9523  uz2m1nn  9551  uz2mulcl  9554  indstr2  9555  qmulz  9569  qre  9571  qnegcl  9582  qreccl  9588  rphalflt  9627  nn0ledivnn  9711  xrltnr  9723  nltpnft  9758  ngtmnft  9761  xrrebnd  9763  xnegcl  9776  xnegneg  9777  xltnegi  9779  xrpnfdc  9786  xrmnfdc  9787  xnegid  9803  xaddid1  9806  xnn0lenn0nn0  9809  xnn0xadd0  9811  xposdif  9826  elioore  9856  elfzuz2  9972  uzsubsubfz  9990  fzdisj  9995  fzmmmeqm  10001  elfz0ubfz0  10068  elfz0fzfz0  10069  fz0fzelfz0  10070  fz0fzdiffz0  10073  elfzmlbp  10075  difelfzle  10077  difelfznle  10078  nn0disj  10081  2ffzeq  10084  fzo1fzo0n0  10126  elfzo0z  10127  elfzo0le  10128  fzonmapblen  10130  fzofzim  10131  elfzodifsumelfzo  10144  elfzonlteqm1  10153  fzonn0p1p1  10156  elfzom1p1elfzo  10157  ssfzo12bi  10168  ubmelm1fzo  10169  fzind2  10182  subfzo0  10185  rebtwn2z  10198  fldiv4p1lem1div2  10248  flqeqceilz  10261  zmodidfzoimp  10297  modfzo0difsn  10338  nnsinds  10386  nn0sinds  10387  expcl2lemap  10475  qexpclz  10484  facp1  10651  facnn2  10655  faclbnd3  10664  bcn1  10679  hashfz0  10747  cvg1nlemres  10936  rexanuz  10939  fclim  11244  climmo  11248  iser3shft  11296  fsumsplitsn  11360  fsum2dlemstep  11384  fisumcom2  11388  arisum  11448  arisum2  11449  prodmodc  11528  fprodfac  11565  fprod2dlemstep  11572  fprodcom2fi  11576  fprodsplitsn  11583  eftlub  11640  ef01bndlem  11706  sin01gt0  11711  cos01gt0  11712  sin02gt0  11713  dvdsdivcl  11797  addmodlteqALT  11806  odd2np1  11819  oddge22np1  11827  m1expe  11845  nn0enne  11848  nn0o1gt2  11851  nno  11852  ndvdsadd  11877  infssuzcldc  11893  dfgcd2  11956  mulgcd  11958  algfx  11993  prmind2  12061  prm2orodd  12067  prmgt1  12073  oddprmgt2  12075  dfphi2  12161  nnnn0modprm0  12196  prm23lt5  12204  pythagtriplem2  12207  pcz  12272  dvdsprmpweqnn  12276  oddprmdvds  12293  prmunb  12301  4sqlem4  12331  evenennn  12335  distop  12838  ntrss  12872  ssntr  12875  lmrcl  12944  lmreltop  12946  txuni2  13009  txcn  13028  hmeocnvb  13071  xmetunirn  13111  blssioo  13298  divcnap  13308  cdivcncfap  13340  dedekindeulemlub  13351  dedekindicclemlub  13360  dvexp2  13429  pilem3  13457  sincosq1sgn  13500  sincosq2sgn  13501  sincosq3sgn  13502  sincosq4sgn  13503  sinq12gt0  13504  zabsle1  13653  lgsdir2lem4  13685  2sqlem2  13704  2sqlem10  13714  bj-pm2.18st  13744  bj-dcstab  13750  decidi  13789  sumdc2  13793  bj-charfunbi  13806  bdel  13840  bdssex  13897  bj-indind  13927  findset  13940  nninfall  14002  trirec0  14036