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-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  sylbb  122  sylbb2  137  3imtr4i  200  simplbiim  382  mpan10  461  an12s  535  an32s  538  an4s  558  sylnbi  644  condc  793  notnotrdc  795  pm2.61ddc  802  pm5.18dc  821  dcim  828  pm2.25dc  836  pm2.85dc  855  pm5.12dc  860  pm5.14dc  861  pm5.55dc  863  peircedc  864  pm5.54dc  871  dcor  887  pm5.62dc  897  pm5.63dc  898  pm4.83dc  903  3simpb  947  3simpc  948  3imp  1143  3com12  1153  3com13  1154  syl3anb  1227  xoranor  1323  xorbin  1330  xordc1  1339  biassdc  1341  nfr  1466  nfand  1515  19.21t  1529  19.30dc  1574  exintrbi  1580  19.9t  1589  nfnt  1602  equveli  1700  exdistrfor  1739  sbcof2  1749  sbidm  1790  sbi1v  1830  sbalyz  1935  sbal1yz  1937  nfsb4t  1950  euex  1990  eumo0  1991  mor  2002  exmodc  2010  mo3h  2013  mopick  2038  moexexdc  2044  euexex  2045  2euex  2047  exists2  2057  eqcoms  2103  eleq2s  2194  nfcr  2232  necon3ai  2316  rexnalim  2386  dfrex2dc  2387  rexex  2438  rsp  2439  ralim  2450  rexim  2485  r19.32r  2536  r19.44av  2548  r19.45av  2549  gencl  2673  gencbvex  2687  gencbval  2689  vtoclgf  2699  vtoclg1f  2700  pm13.183  2776  elrabi  2790  eueq2dc  2810  eueq3dc  2811  mob2  2817  euxfr2dc  2822  reu3  2827  rmoim  2838  2rmorex  2843  sbcex  2870  sbcbi2  2911  ra5  2949  sseq1  3070  difdif  3148  dfss4st  3256  difindiss  3277  undif3ss  3284  dfrab3ss  3301  abvor0dc  3333  reldisj  3361  disjel  3364  inssdif0im  3377  uneqdifeqim  3395  r19.2m  3396  r19.2mOLD  3397  r19.3rm  3398  r19.9rmv  3401  rexm  3409  ralm  3414  raaanlem  3415  ifnefalse  3432  ifandc  3455  ifmdc  3456  nelpri  3498  nelprd  3500  prprc1  3578  difprsn2  3607  diftpsn3  3608  snsssn  3635  preqr2  3643  preq12b  3644  opthpr  3646  prneimg  3648  oprcl  3676  pwprss  3679  intmin4  3746  uniintabim  3755  dfiin2g  3793  iinss2  3812  iundif2ss  3825  disjnim  3866  disjnims  3867  invdisj  3869  disjiun  3870  trel  3973  trss  3975  ssex  4005  bnd2  4037  abssexg  4046  exmidexmid  4060  rext  4075  unipw  4077  euabex  4085  mss  4086  exss  4087  copsexg  4104  opelopabsb  4120  pwssunim  4144  epelg  4150  sowlin  4180  sotritric  4184  elsuci  4263  sucprc  4272  reusv3  4319  ordon  4340  onsucmin  4361  onsucelsucr  4362  unon  4365  onsucelsucexmid  4383  setind  4392  setind2  4393  sucprcreg  4402  en2lp  4407  eunex  4414  ordsoexmid  4415  ordpwsucss  4420  tfi  4434  peano1  4446  peano2  4447  find  4451  0nelelxp  4506  opelxp  4507  elvvuni  4541  optocl  4553  ralxpf  4623  rexxpf  4624  relop  4627  breldm  4681  dmxpm  4697  elreldm  4703  dmrnssfld  4738  dmcosseq  4746  resabs1  4784  resima2  4789  issref  4857  asymref  4860  xpidtr  4865  trin2  4866  poirr2  4867  xpmlem  4895  dmxpss  4905  xp11m  4913  cnveqb  4930  dfco2a  4975  cores2  4987  coi2  4991  relcnvtr  4994  relresfld  5004  relcnvexb  5014  cnviinm  5016  iotauni  5036  iota1  5038  iota4  5042  dffun8  5087  funcnvsn  5104  imadif  5139  imainlem  5140  fcoi1  5239  fcoi2  5240  f0rn0  5253  f1ocnv  5314  f1ocnvb  5315  fun11iun  5322  ffoss  5333  f1o00  5336  fo00  5337  relelfvdm  5385  nfvres  5386  nfunsn  5387  ssimaex  5414  fvmptss2  5428  fvmptssdm  5437  unpreima  5477  respreima  5480  elrnrexdm  5491  elrnrexdmb  5492  rexrnmpt  5495  dffo4  5500  rnmptss  5513  fvpr1  5556  fvpr2  5557  elunirn  5599  f1veqaeq  5602  isores1  5647  riotauni  5668  riotacl2  5675  riota1  5680  riota1a  5681  snriota  5691  eusvobj2  5692  acexmidlema  5697  acexmidlemb  5698  acexmidlem2  5703  oprabid  5735  0neqopab  5748  brabvv  5749  1stval2  5984  2ndval2  5985  xp1st  5994  xp2nd  5995  unielxp  6002  releldm2  6013  cnvf1o  6052  fo2ndf  6054  poxp  6059  reldmtpos  6080  dftpos4  6090  tpostpos  6091  tpostpos2  6092  iunon  6111  smoel  6127  tfrlem4  6140  tfrlem7  6144  tfrlem8  6145  tfrlem9  6146  nnaord  6335  ecexr  6364  swoord1  6388  swoord2  6389  0er  6393  mapprc  6476  mapsnconst  6518  ixpf  6544  mptelixpg  6558  idssen  6601  ener  6603  en0  6619  en1  6623  en1bg  6624  2dom  6629  enm  6643  xpsnen  6644  ssenen  6674  snnen2og  6682  php5dom  6686  phpm  6688  findcard  6711  findcard2  6712  findcard2s  6713  unfiexmid  6735  fiintim  6746  fidcenumlemim  6768  sbthlem1  6773  djuexb  6844  djuss  6870  eldju2ndl  6872  eldju2ndr  6873  ctssdclemr  6911  exmidlpo  6927  finnum  6950  exmidfodomrlemim  6966  indpi  7051  subhalfnqq  7123  archnqq  7126  enq0sym  7141  nqnq0pi  7147  nqnq0  7150  mulnnnq0  7159  prml  7186  prmu  7187  prssnql  7188  prssnqu  7189  prcdnql  7193  prcunqu  7194  prltlu  7196  prnmaxl  7197  prnminu  7198  prloc  7200  prdisj  7201  addcanprg  7325  recexprlemopl  7334  recexprlemopu  7336  cauappcvgprlemladdfu  7363  caucvgprlemladdfu  7386  recexgt0sr  7469  renfdisj  7696  negf1o  8011  recexre  8206  apsqgt0  8229  apreim  8231  recexaplem2  8274  rerecclap  8351  nn0ge0  8854  elnnnn0b  8873  xnn0xr  8897  xnn0nemnf  8903  xnn0nnn0pnf  8905  znegcl  8937  zeo  9008  nn0ind  9017  nn0ind-raph  9020  uzn0  9191  eluzaddi  9202  eluzsubi  9203  uznn0sub  9207  uz3m2nn  9218  uznnssnn  9222  uz2m1nn  9249  uz2mulcl  9252  indstr2  9253  qmulz  9265  qre  9267  qnegcl  9278  qreccl  9284  rphalflt  9320  nn0ledivnn  9395  xrltnr  9407  nltpnft  9438  ngtmnft  9441  xrrebnd  9443  xnegcl  9456  xnegneg  9457  xltnegi  9459  xrpnfdc  9466  xrmnfdc  9467  xnegid  9483  xaddid1  9486  xnn0lenn0nn0  9489  xnn0xadd0  9491  xposdif  9506  elioore  9536  elfzuz2  9650  uzsubsubfz  9668  fzdisj  9673  fzmmmeqm  9679  elfz0ubfz0  9743  elfz0fzfz0  9744  fz0fzelfz0  9745  fz0fzdiffz0  9748  elfzmlbp  9750  difelfzle  9752  difelfznle  9753  nn0disj  9756  2ffzeq  9759  fzo1fzo0n0  9801  elfzo0z  9802  elfzo0le  9803  fzonmapblen  9805  fzofzim  9806  elfzodifsumelfzo  9819  elfzonlteqm1  9828  fzonn0p1p1  9831  elfzom1p1elfzo  9832  ssfzo12bi  9843  ubmelm1fzo  9844  fzind2  9857  subfzo0  9860  rebtwn2z  9873  fldiv4p1lem1div2  9919  flqeqceilz  9932  zmodidfzoimp  9968  modfzo0difsn  10009  nnsinds  10057  nn0sinds  10058  expcl2lemap  10146  qexpclz  10155  facp1  10317  facnn2  10321  faclbnd3  10330  bcn1  10345  hashfz0  10412  cvg1nlemres  10597  rexanuz  10600  fclim  10902  climmo  10906  iser3shft  10954  fsumsplitsn  11018  fsum2dlemstep  11042  fisumcom2  11046  arisum  11106  arisum2  11107  eftlub  11194  ef01bndlem  11261  sin01gt0  11266  cos01gt0  11267  sin02gt0  11268  dvdsdivcl  11343  addmodlteqALT  11352  odd2np1  11365  oddge22np1  11373  m1expe  11391  nn0enne  11394  nn0o1gt2  11397  nno  11398  ndvdsadd  11423  infssuzcldc  11439  dfgcd2  11495  mulgcd  11497  algfx  11526  prmind2  11594  prm2orodd  11600  prmgt1  11605  oddprmgt2  11607  dfphi2  11688  evenennn  11698  distop  12036  ntrss  12070  ssntr  12073  lmrcl  12142  lmreltop  12144  txuni2  12206  txcn  12225  xmetunirn  12286  blssioo  12464  cdivcncfap  12499  bj-nfalt  12553  decidi  12583  sumdc2  12587  bdel  12624  bdssex  12681  bj-indind  12715  findset  12728  nninfall  12788