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  827  notnotrdc  829  const  838  condcOLD  840  pm2.61ddc  847  pm5.18dc  869  pm2.25dc  879  pm2.85dc  891  pm5.12dc  896  pm5.14dc  897  pm5.55dc  899  peircedc  900  pm5.54dc  904  dcor  920  pm5.62dc  930  pm5.63dc  931  pm4.83dc  936  3simpb  980  3simpc  981  3imp  1176  3com12  1186  3com13  1187  syl3anb  1260  xoranor  1356  xorbin  1363  xordc1  1372  biassdc  1374  nfr  1499  nfand  1548  19.21t  1562  19.30dc  1607  exintrbi  1613  19.9t  1622  nfnt  1635  equveli  1733  exdistrfor  1773  sbcof2  1783  sbidm  1824  sbi1v  1864  sbalyz  1975  sbal1yz  1977  nfsb4t  1990  euex  2030  eumo0  2031  mor  2042  exmodc  2050  mo3h  2053  mopick  2078  moexexdc  2084  euexex  2085  2euex  2087  exists2  2097  eqcoms  2143  eleq2s  2235  nfcr  2274  necon3ai  2358  rexnalim  2428  dfrex2dc  2429  rexex  2482  rsp  2483  ralim  2494  rexim  2529  r19.32r  2581  r19.44av  2593  r19.45av  2594  gencl  2721  gencbvex  2735  gencbval  2737  vtoclgf  2747  vtoclg1f  2748  pm13.183  2826  elrabi  2841  eueq2dc  2861  eueq3dc  2862  mob2  2868  euxfr2dc  2873  reu3  2878  rmoim  2889  2rmorex  2894  sbcex  2921  sbcbi2  2963  ra5  3001  sseq1  3125  difdif  3206  dfss4st  3314  difindiss  3335  undif3ss  3342  dfrab3ss  3359  abvor0dc  3391  reldisj  3419  disjel  3422  inssdif0im  3435  uneqdifeqim  3453  r19.2m  3454  r19.2mOLD  3455  r19.3rm  3456  r19.9rmv  3459  rexm  3467  ralm  3472  raaanlem  3473  ifnefalse  3490  ifandc  3513  ifmdc  3514  nelpri  3556  nelprd  3558  prprc1  3639  difprsn2  3668  diftpsn3  3669  snsssn  3696  preqr2  3704  preq12b  3705  opthpr  3707  prneimg  3709  oprcl  3737  pwprss  3740  intmin4  3807  uniintabim  3816  dfiin2g  3854  iinss2  3873  iundif2ss  3886  disjnim  3928  disjnims  3929  invdisj  3931  disjiun  3932  brne0  3985  brm  3986  trel  4041  trss  4043  ssex  4073  bnd2  4105  abssexg  4114  exmidexmid  4128  rext  4145  unipw  4147  euabex  4155  mss  4156  exss  4157  copsexg  4174  opelopabsb  4190  pwssunim  4214  epelg  4220  sowlin  4250  sotritric  4254  elsuci  4333  sucprc  4342  reusv3  4389  ordon  4410  onsucmin  4431  onsucelsucr  4432  unon  4435  onsucelsucexmid  4453  setind  4462  setind2  4463  sucprcreg  4472  en2lp  4477  eunex  4484  ordsoexmid  4485  ordpwsucss  4490  tfi  4504  peano1  4516  peano2  4517  find  4521  0nelelxp  4576  opelxp  4577  elvvuni  4611  optocl  4623  ralxpf  4693  rexxpf  4694  relop  4697  breldm  4751  dmxpm  4767  elreldm  4773  dmrnssfld  4810  dmcosseq  4818  resabs1  4856  resima2  4861  issref  4929  asymref  4932  xpidtr  4937  trin2  4938  poirr2  4939  xpmlem  4967  dmxpss  4977  xp11m  4985  cnveqb  5002  dfco2a  5047  cores2  5059  coi2  5063  relcnvtr  5066  relresfld  5076  relcnvexb  5086  cnviinm  5088  iotauni  5108  iota1  5110  iota4  5114  dffun8  5159  funcnvsn  5176  imadif  5211  imainlem  5212  fcoi1  5311  fcoi2  5312  f0rn0  5325  f1ocnv  5388  f1ocnvb  5389  fun11iun  5396  ffoss  5407  f1o00  5410  fo00  5411  relelfvdm  5461  nfvres  5462  nfunsn  5463  ssimaex  5490  fvmptss2  5504  fvmptssdm  5513  unpreima  5553  respreima  5556  elrnrexdm  5567  elrnrexdmb  5568  rexrnmpt  5571  dffo4  5576  rnmptss  5589  fvpr1  5632  fvpr2  5633  elunirn  5675  f1veqaeq  5678  isores1  5723  riotauni  5744  riotacl2  5751  riota1  5756  riota1a  5757  snriota  5767  eusvobj2  5768  acexmidlema  5773  acexmidlemb  5774  acexmidlem2  5779  oprabid  5811  0neqopab  5824  brabvv  5825  1stval2  6061  2ndval2  6062  xp1st  6071  xp2nd  6072  unielxp  6080  releldm2  6091  cnvf1o  6130  fo2ndf  6132  poxp  6137  reldmtpos  6158  dftpos4  6168  tpostpos  6169  tpostpos2  6170  iunon  6189  smoel  6205  tfrlem4  6218  tfrlem7  6222  tfrlem8  6223  tfrlem9  6224  nnaord  6413  ecexr  6442  swoord1  6466  swoord2  6467  0er  6471  mapprc  6554  mapsnconst  6596  ixpf  6622  mptelixpg  6636  idssen  6679  ener  6681  en0  6697  en1  6701  en1bg  6702  2dom  6707  enm  6722  xpsnen  6723  ssenen  6753  snnen2og  6761  php5dom  6765  phpm  6767  findcard  6790  findcard2  6791  findcard2s  6792  unfiexmid  6814  fiintim  6825  fidcenumlemim  6848  sbthlem1  6853  fiss  6873  djuexb  6937  djuss  6963  eldju2ndl  6965  eldju2ndr  6966  ctssdclemr  7005  exmidlpo  7023  finnum  7056  exmidfodomrlemim  7074  indpi  7174  subhalfnqq  7246  archnqq  7249  enq0sym  7264  nqnq0pi  7270  nqnq0  7273  mulnnnq0  7282  prml  7309  prmu  7310  prssnql  7311  prssnqu  7312  prcdnql  7316  prcunqu  7317  prltlu  7319  prnmaxl  7320  prnminu  7321  prloc  7323  prdisj  7324  addcanprg  7448  recexprlemopl  7457  recexprlemopu  7459  cauappcvgprlemladdfu  7486  caucvgprlemladdfu  7509  recexgt0sr  7605  renfdisj  7848  axsuploc  7861  negf1o  8168  recexre  8364  apsqgt0  8387  apreim  8389  aprcl  8432  recexaplem2  8437  rerecclap  8514  nn0ge0  9026  elnnnn0b  9045  xnn0xr  9069  xnn0nemnf  9075  xnn0nnn0pnf  9077  znegcl  9109  zeo  9180  nn0ind  9189  nn0ind-raph  9192  uzn0  9365  eluzaddi  9376  eluzsubi  9377  uznn0sub  9381  uz3m2nn  9395  uznnssnn  9399  uz2m1nn  9426  uz2mulcl  9429  indstr2  9430  qmulz  9442  qre  9444  qnegcl  9455  qreccl  9461  rphalflt  9500  nn0ledivnn  9584  xrltnr  9596  nltpnft  9627  ngtmnft  9630  xrrebnd  9632  xnegcl  9645  xnegneg  9646  xltnegi  9648  xrpnfdc  9655  xrmnfdc  9656  xnegid  9672  xaddid1  9675  xnn0lenn0nn0  9678  xnn0xadd0  9680  xposdif  9695  elioore  9725  elfzuz2  9840  uzsubsubfz  9858  fzdisj  9863  fzmmmeqm  9869  elfz0ubfz0  9933  elfz0fzfz0  9934  fz0fzelfz0  9935  fz0fzdiffz0  9938  elfzmlbp  9940  difelfzle  9942  difelfznle  9943  nn0disj  9946  2ffzeq  9949  fzo1fzo0n0  9991  elfzo0z  9992  elfzo0le  9993  fzonmapblen  9995  fzofzim  9996  elfzodifsumelfzo  10009  elfzonlteqm1  10018  fzonn0p1p1  10021  elfzom1p1elfzo  10022  ssfzo12bi  10033  ubmelm1fzo  10034  fzind2  10047  subfzo0  10050  rebtwn2z  10063  fldiv4p1lem1div2  10109  flqeqceilz  10122  zmodidfzoimp  10158  modfzo0difsn  10199  nnsinds  10247  nn0sinds  10248  expcl2lemap  10336  qexpclz  10345  facp1  10508  facnn2  10512  faclbnd3  10521  bcn1  10536  hashfz0  10603  cvg1nlemres  10789  rexanuz  10792  fclim  11095  climmo  11099  iser3shft  11147  fsumsplitsn  11211  fsum2dlemstep  11235  fisumcom2  11239  arisum  11299  arisum2  11300  prodmodc  11379  eftlub  11433  ef01bndlem  11499  sin01gt0  11504  cos01gt0  11505  sin02gt0  11506  dvdsdivcl  11584  addmodlteqALT  11593  odd2np1  11606  oddge22np1  11614  m1expe  11632  nn0enne  11635  nn0o1gt2  11638  nno  11639  ndvdsadd  11664  infssuzcldc  11680  dfgcd2  11738  mulgcd  11740  algfx  11769  prmind2  11837  prm2orodd  11843  prmgt1  11848  oddprmgt2  11850  dfphi2  11932  evenennn  11942  distop  12293  ntrss  12327  ssntr  12330  lmrcl  12399  lmreltop  12401  txuni2  12464  txcn  12483  hmeocnvb  12526  xmetunirn  12566  blssioo  12753  divcnap  12763  cdivcncfap  12795  dedekindeulemlub  12806  dedekindicclemlub  12815  dvexp2  12884  pilem3  12912  sincosq1sgn  12955  sincosq2sgn  12956  sincosq3sgn  12957  sincosq4sgn  12958  sinq12gt0  12959  bj-pm2.18st  13129  bj-dcstab  13132  decidi  13173  sumdc2  13177  bdel  13214  bdssex  13271  bj-indind  13301  findset  13314  nninfall  13379  trirec0  13412