Theorem sylbi 119

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sylbb  121  sylbb2  136  3imtr4i  199  simplbiim  379  mpan10  457  an12s  529  an32s  532  an4s  552  sylnbi  635  condc  782  notnotrdc  784  pm2.61ddc  791  pm5.18dc  810  dcim  817  pm2.25dc  825  pm2.85dc  844  pm5.12dc  849  pm5.14dc  850  pm5.55dc  852  peircedc  853  pm5.54dc  860  dcor  876  pm5.62dc  886  pm5.63dc  887  pm4.83dc  892  3simpb  936  3simpc  937  3imp  1132  3com12  1142  3com13  1143  syl3anb  1212  xoranor  1308  xorbin  1315  xordc1  1324  biassdc  1326  nfr  1451  nfand  1500  19.21t  1514  19.30dc  1558  exintrbi  1564  19.9t  1573  nfnt  1586  equveli  1682  exdistrfor  1721  sbcof2  1731  sbidm  1772  sbi1v  1812  sbalyz  1916  sbal1yz  1918  nfsb4t  1931  euex  1971  eumo0  1972  mor  1983  exmodc  1991  mo3h  1994  mopick  2019  moexexdc  2025  euexex  2026  2euex  2028  exists2  2038  eqcoms  2084  eleq2s  2173  nfcr  2211  necon3ai  2294  rexnalim  2359  rexex  2410  rsp  2411  ralim  2422  rexim  2455  r19.32r  2501  r19.44av  2513  r19.45av  2514  gencl  2631  gencbvex  2645  gencbval  2647  vtoclgf  2657  pm13.183  2732  elrabi  2746  eueq2dc  2765  eueq3dc  2766  mob2  2772  euxfr2dc  2777  reu3  2782  rmoim  2791  2rmorex  2796  sbcex  2823  sbcbi2  2864  ra5  2902  sseq1  3020  difdif  3097  difindiss  3218  undif3ss  3225  dfrab3ss  3242  abvor0dc  3269  reldisj  3295  disjel  3298  inssdif0im  3311  uneqdifeqim  3328  r19.2m  3329  r19.3rm  3330  r19.9rmv  3333  rexm  3340  ralm  3345  raaanlem  3346  ifnefalse  3362  nelpri  3422  prprc1  3500  difprsn2  3526  diftpsn3  3527  snsssn  3553  preqr2  3561  preq12b  3562  opthpr  3564  prneimg  3566  oprcl  3594  pwprss  3597  intmin4  3664  uniintabim  3673  dfiin2g  3711  iinss2  3730  iundif2ss  3743  invdisj  3780  trel  3882  trss  3884  ssex  3915  bnd2  3947  abssexg  3955  rext  3970  unipw  3972  euabex  3980  mss  3981  exss  3982  copsexg  3999  opelopabsb  4015  pwssunim  4039  epelg  4045  sowlin  4075  sotritric  4079  elsuci  4158  sucprc  4167  reusv3  4210  ordon  4230  onsucmin  4251  onsucelsucr  4252  unon  4255  onsucelsucexmid  4273  setind  4282  setind2  4283  sucprcreg  4292  en2lp  4297  eunex  4304  ordsoexmid  4305  ordpwsucss  4310  tfi  4323  peano1  4335  peano2  4336  find  4340  0nelelxp  4391  opelxp  4392  elvvuni  4422  optocl  4434  ralxpf  4500  rexxpf  4501  relop  4504  breldm  4557  dmxpm  4573  elreldm  4578  dmrnssfld  4613  dmcosseq  4621  resabs1  4658  resima2  4662  issref  4727  asymref  4730  xpidtr  4735  trin2  4736  poirr2  4737  xpmlem  4764  dmxpss  4773  xp11m  4779  cnveqb  4796  dfco2a  4841  cores2  4853  coi2  4857  relcnvtr  4860  relresfld  4867  relcnvexb  4877  cnviinm  4879  iotauni  4899  iota1  4901  iota4  4905  dffun8  4949  funcnvsn  4965  imadif  4999  imainlem  5000  fcoi1  5090  fcoi2  5091  f1ocnv  5159  f1ocnvb  5160  fun11iun  5167  ffoss  5178  f1o00  5181  fo00  5182  relelfvdm  5226  nfvres  5227  nfunsn  5228  ssimaex  5255  fvmptss2  5268  fvmptssdm  5276  unpreima  5313  respreima  5316  elrnrexdm  5327  elrnrexdmb  5328  rexrnmpt  5331  dffo4  5336  rnmptss  5347  fvpr1  5386  fvpr2  5387  elunirn  5426  f1veqaeq  5429  isores1  5474  riotauni  5494  riotacl2  5501  riota1  5506  riota1a  5507  snriota  5517  eusvobj2  5518  acexmidlema  5523  acexmidlemb  5524  acexmidlem2  5529  oprabid  5557  0neqopab  5570  brabvv  5571  1stval2  5802  2ndval2  5803  xp1st  5812  xp2nd  5813  unielxp  5820  releldm2  5831  cnvf1o  5866  fo2ndf  5868  poxp  5873  reldmtpos  5891  dftpos4  5901  tpostpos  5902  tpostpos2  5903  iunon  5922  smoel  5938  tfrlem4  5952  tfrlem7  5956  tfrlem8  5957  tfrlem9  5958  nnaord  6105  ecexr  6134  swoord1  6158  swoord2  6159  0er  6163  idssen  6280  ener  6282  en0  6298  en1  6302  en1bg  6303  2dom  6308  enm  6317  xpsnen  6318  snnen2og  6345  php5dom  6349  phpm  6351  findcard  6372  findcard2  6373  findcard2s  6374  finnum  6452  indpi  6532  subhalfnqq  6604  archnqq  6607  enq0sym  6622  nqnq0pi  6628  nqnq0  6631  mulnnnq0  6640  prml  6667  prmu  6668  prssnql  6669  prssnqu  6670  prcdnql  6674  prcunqu  6675  prltlu  6677  prnmaxl  6678  prnminu  6679  prloc  6681  prdisj  6682  addcanprg  6806  recexprlemopl  6815  recexprlemopu  6817  cauappcvgprlemladdfu  6844  caucvgprlemladdfu  6867  recexgt0sr  6950  renfdisj  7172  negf1o  7486  recexre  7678  apsqgt0  7701  apreim  7703  recexaplem2  7742  rerecclap  7818  nn0ge0  8313  elnnnn0b  8332  znegcl  8382  zeo  8452  nn0ind  8461  nn0ind-raph  8464  uzn0  8634  eluzaddi  8645  eluzsubi  8646  uznn0sub  8650  uz3m2nn  8661  uznnssnn  8665  uz2m1nn  8692  uz2mulcl  8695  indstr2  8696  qmulz  8708  qre  8710  qnegcl  8721  qreccl  8727  rphalflt  8763  nn0ledivnn  8838  xrltnr  8855  nltpnft  8884  ngtmnft  8885  xrrebnd  8886  xnegcl  8899  xnegneg  8900  xltnegi  8902  elioore  8935  elfzuz2  9048  uzsubsubfz  9066  fzdisj  9071  fzmmmeqm  9076  elfz0ubfz0  9136  elfz0fzfz0  9137  fz0fzelfz0  9138  fz0fzdiffz0  9141  elfzmlbp  9143  difelfzle  9145  difelfznle  9146  nn0disj  9148  2ffzeq  9151  fzo1fzo0n0  9192  elfzo0z  9193  elfzo0le  9194  fzonmapblen  9196  fzofzim  9197  elfzodifsumelfzo  9210  elfzonlteqm1  9219  fzonn0p1p1  9222  elfzom1p1elfzo  9223  ssfzo12bi  9234  ubmelm1fzo  9235  fzind2  9248  subfzo0  9251  rebtwn2z  9263  fldiv4p1lem1div2  9307  flqeqceilz  9320  zmodidfzoimp  9356  modfzo0difsn  9397  nnsinds  9429  nn0sinds  9430  expcl2lemap  9488  qexpclz  9497  facp1  9657  facnn2  9661  faclbnd3  9670  bcn1  9685  cvg1nlemres  9871  rexanuz  9874  fclim  10133  climmo  10137  dvdsdivcl  10250  addmodlteqALT  10259  odd2np1  10272  oddge22np1  10281  m1expe  10299  nn0enne  10302  nn0o1gt2  10305  nno  10306  ndvdsadd  10331  infssuzcldc  10347  dfgcd2  10403  mulgcd  10405  ialgfx  10434  prmind2  10502  prm2orodd  10508  prmgt1  10513  oddprmgt2  10515  bj-nfalt  10575  bdel  10636  bdssex  10693  bj-indind  10727  findset  10740