Theorem sylbi 121

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

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylbb  123  sylbb2  138  3imtr4i  201  simplbiim  387  mpan10  474  an12s  565  an32s  568  an4s  588  sylnbi  680  dcim  843  notnotrdc  845  condcOLD  856  pm2.61ddc  863  pm5.18dc  885  pm2.25dc  895  pm2.85dc  907  pm5.12dc  912  pm5.14dc  913  pm5.55dc  915  peircedc  916  pm5.54dc  920  dcand  935  dcor  938  pm5.62dc  948  pm5.63dc  949  pm4.83dc  954  3simpb  998  3simpc  999  3imp  1196  3com12  1210  3com13  1211  syl3anb  1293  xoranor  1397  xorbin  1404  xordc1  1413  biassdc  1415  nfr  1542  nfand  1592  19.21t  1606  19.30dc  1651  exintrbi  1657  19.9t  1666  nfnt  1680  equveli  1783  exdistrfor  1824  sbcof2  1834  sbidm  1875  sbi1v  1916  sbalyz  2028  sbal1yz  2030  nfsb4t  2043  euex  2085  eumo0  2086  mor  2097  exmodc  2105  mo3h  2108  mopick  2133  moexexdc  2139  euexex  2140  2euex  2142  exists2  2152  eqcoms  2209  eleq2s  2301  nfcr  2341  necon3ai  2426  rexnalim  2496  dfrex2dc  2498  rexex  2553  rsp  2554  ralim  2566  rexim  2601  r19.32r  2653  r19.44av  2666  r19.45av  2667  gencl  2806  gencbvex  2821  gencbval  2823  vtoclgf  2833  vtoclg1f  2834  pm13.183  2915  elrabi  2930  eueq2dc  2950  eueq3dc  2951  mob2  2957  euxfr2dc  2962  reu3  2967  rmoim  2978  2rmorex  2983  sbcex  3011  sbcbi2  3053  ra5  3091  sseq1  3220  difdif  3302  dfss4st  3410  difindiss  3431  undif3ss  3438  dfrab3ss  3455  abvor0dc  3488  reldisj  3516  disjel  3519  inssdif0im  3532  uneqdifeqim  3550  r19.2m  3551  r19.2mOLD  3552  r19.3rm  3553  r19.9rmv  3556  rexm  3564  ralm  3568  raaanlem  3569  ifnefalse  3586  ifnotdc  3614  ifandc  3615  ifmdc  3617  nelpri  3662  nelprd  3664  prprc1  3746  difprsn2  3779  diftpsn3  3780  snsssn  3808  preqr2  3816  preq12b  3817  opthpr  3819  prneimg  3821  oprcl  3849  pwprss  3852  intmin4  3919  uniintabim  3928  dfiin2g  3966  iinss2  3986  iundif2ss  3999  disjnim  4041  disjnims  4042  invdisj  4044  disjiun  4046  brne0  4101  brm  4102  trel  4157  trss  4159  ssex  4189  bnd2  4225  abssexg  4234  exmidexmid  4248  rext  4267  unipw  4269  euabex  4277  mss  4278  exss  4279  copsexg  4296  opelopabsb  4314  pwssunim  4339  epelg  4345  sowlin  4375  sotritric  4379  elsuci  4458  sucprc  4467  reusv3  4515  ordon  4542  onsucmin  4563  onsucelsucr  4564  unon  4567  onsucelsucexmid  4586  setind  4595  setind2  4596  sucprcreg  4605  en2lp  4610  eunex  4617  ordsoexmid  4618  ordpwsucss  4623  tfi  4638  peano1  4650  peano2  4651  find  4655  0nelelxp  4712  opelxp  4713  elvvuni  4747  optocl  4759  ralxpf  4832  rexxpf  4833  relop  4836  breldm  4891  dmxpm  4907  elreldm  4913  dmrnssfld  4950  dmcosseq  4959  resabs1  4997  resima2  5002  issref  5074  asymref  5077  xpidtr  5082  trin2  5083  poirr2  5084  xpmlem  5112  dmxpss  5122  xp11m  5130  cnveqb  5147  dfco2a  5192  cores2  5204  coi2  5208  relcnvtr  5211  relresfld  5221  relcnvexb  5231  cnviinm  5233  iotauni  5253  iota1  5255  iota4  5260  iotam  5272  dffun8  5308  fununfun  5326  funcnvsn  5328  imadif  5363  imainlem  5364  fcoi1  5468  fcoi2  5469  f0rn0  5482  f1ocnv  5547  f1ocnvb  5548  fun11iun  5555  ffoss  5566  f1o00  5570  fo00  5571  relelfvdm  5621  nfvres  5623  nfunsn  5624  ssimaex  5653  fvmptss2  5667  fvmptssdm  5677  unpreima  5718  respreima  5721  elrnrexdm  5732  elrnrexdmb  5733  rexrnmpt  5736  dffo4  5741  rnmptss  5754  funiun  5774  funopdmsn  5777  fvpr1  5801  fvpr2  5802  elunirn  5848  f1veqaeq  5851  isores1  5896  iotaexel  5917  riotauni  5919  riotacl2  5926  riota1  5931  riota1a  5932  snriota  5942  eusvobj2  5943  acexmidlema  5948  acexmidlemb  5949  acexmidlem2  5954  oprabid  5989  0neqopab  6003  brabvv  6004  1stval2  6254  2ndval2  6255  xp1st  6264  xp2nd  6265  unielxp  6273  releldm2  6284  cnvf1o  6324  fo2ndf  6326  poxp  6331  reldmtpos  6352  dftpos4  6362  tpostpos  6363  tpostpos2  6364  iunon  6383  smoel  6399  tfrlem4  6412  tfrlem7  6416  tfrlem8  6417  tfrlem9  6418  nnaord  6608  ecexr  6638  swoord1  6662  swoord2  6663  0er  6667  mapprc  6752  mapsnconst  6794  ixpf  6820  mptelixpg  6834  idssen  6881  ener  6884  en0  6900  en1  6904  en1bg  6905  2dom  6911  enm  6930  xpsnen  6931  ssenen  6963  snnen2og  6971  php5dom  6975  phpm  6977  findcard  7000  findcard2  7001  findcard2s  7002  unfiexmid  7030  fiintim  7043  fidcenumlemim  7069  sbthlem1  7074  fiss  7094  djuexb  7161  djuss  7187  eldju2ndl  7189  eldju2ndr  7190  ctssdclemr  7229  exmidlpo  7260  finnum  7305  ficardon  7311  exmidfodomrlemim  7325  acnrcl  7329  3nsssucpw1  7367  indpi  7475  subhalfnqq  7547  archnqq  7550  enq0sym  7565  nqnq0pi  7571  nqnq0  7574  mulnnnq0  7583  prml  7610  prmu  7611  prssnql  7612  prssnqu  7613  prcdnql  7617  prcunqu  7618  prltlu  7620  prnmaxl  7621  prnminu  7622  prloc  7624  prdisj  7625  addcanprg  7749  recexprlemopl  7758  recexprlemopu  7760  cauappcvgprlemladdfu  7787  caucvgprlemladdfu  7810  recexgt0sr  7906  renfdisj  8152  axsuploc  8165  negf1o  8474  recexre  8671  apsqgt0  8694  apreim  8696  aprcl  8739  recexaplem2  8745  rerecclap  8823  nn0ge0  9340  elnnnn0b  9359  xnn0xr  9383  xnn0nemnf  9389  xnn0nnn0pnf  9391  znegcl  9423  zeo  9498  nn0ind  9507  nn0ind-raph  9510  uzn0  9684  eluzaddi  9695  eluzsubi  9696  uznn0sub  9700  uz3m2nn  9714  uznnssnn  9718  uz2m1nn  9746  uz2mulcl  9749  indstr2  9750  qmulz  9764  qre  9766  qnegcl  9777  qreccl  9783  rphalflt  9825  nn0ledivnn  9909  xrltnr  9921  nltpnft  9956  ngtmnft  9959  xrrebnd  9961  xnegcl  9974  xnegneg  9975  xltnegi  9977  xrpnfdc  9984  xrmnfdc  9985  xnegid  10001  xaddid1  10004  xnn0lenn0nn0  10007  xnn0xadd0  10009  xposdif  10024  elioore  10054  elfzuz2  10171  uzsubsubfz  10189  fzdisj  10194  fzmmmeqm  10200  elfz0ubfz0  10267  elfz0fzfz0  10268  fz0fzelfz0  10269  fz0fzdiffz0  10272  elfzmlbp  10274  difelfzle  10276  difelfznle  10277  nn0disj  10280  2ffzeq  10283  fzo1fzo0n0  10329  elfzo0z  10330  elfzo0le  10331  fzonmapblen  10333  fzofzim  10334  elfzodifsumelfzo  10352  elfzonlteqm1  10361  fzonn0p1p1  10364  elfzom1p1elfzo  10365  ssfzo12bi  10376  ubmelm1fzo  10377  fzind2  10390  subfzo0  10393  infssuzcldc  10400  rebtwn2z  10419  fldiv4p1lem1div2  10470  fldiv4lem1div2  10472  flqeqceilz  10485  zmodidfzoimp  10521  modfzo0difsn  10562  nnsinds  10612  nn0sinds  10613  expcl2lemap  10718  qexpclz  10727  zzlesq  10875  facp1  10897  facnn2  10901  faclbnd3  10910  bcn1  10925  hashfz0  10992  wrdf  11022  swrdswrdlem  11180  swrdswrd  11181  cvg1nlemres  11371  rexanuz  11374  fclim  11680  climmo  11684  iser3shft  11732  fsumsplitsn  11796  fsum2dlemstep  11820  fisumcom2  11824  arisum  11884  arisum2  11885  prodmodc  11964  fprodfac  12001  fprod2dlemstep  12008  fprodcom2fi  12012  fprodsplitsn  12019  eftlub  12076  ef01bndlem  12142  sin01gt0  12148  cos01gt0  12149  sin02gt0  12150  dvdsdivcl  12236  addmodlteqALT  12245  odd2np1  12259  oddge22np1  12267  m1expe  12285  nn0enne  12288  nn0o1gt2  12291  nno  12292  ndvdsadd  12317  dfgcd2  12410  mulgcd  12412  algfx  12449  prmind2  12517  prm2orodd  12523  prmgt1  12529  oddprmgt2  12531  dfphi2  12617  nnnn0modprm0  12653  prm23lt5  12661  pythagtriplem2  12664  pcz  12730  dvdsprmpweqnn  12734  oddprmdvds  12752  prmunb  12760  4sqlem4  12790  4sqlem19  12807  evenennn  12839  fngsum  13295  igsumvalx  13296  dfgrp3me  13507  mulgnn0gsum  13539  rngdi  13777  rngdir  13778  dvdsrcl2  13936  unitinvcl  13960  unitinvinv  13961  unitlinv  13963  unitrinv  13964  rmodislmodlem  14187  rmodislmod  14188  zrhval  14454  psrbagf  14507  distop  14632  ntrss  14666  ssntr  14669  lmrcl  14738  lmreltop  14740  txuni2  14803  txcn  14822  hmeocnvb  14865  xmetunirn  14905  blssioo  15100  divcnap  15112  cdivcncfap  15151  dedekindeulemlub  15167  dedekindicclemlub  15176  dvexp2  15259  elply2  15282  plyco  15306  pilem3  15330  sincosq1sgn  15373  sincosq2sgn  15374  sincosq3sgn  15375  sincosq4sgn  15376  sinq12gt0  15377  fsumdvdsmul  15538  zabsle1  15551  lgsdir2lem4  15583  gausslemma2dlem0f  15606  gausslemma2dlem1a  15610  gausslemma2dlem2  15614  gausslemma2dlem3  15615  gausslemma2dlem4  15616  2lgslem1a1  15638  2lgslem3  15653  2lgsoddprmlem3  15663  2lgsoddprm  15665  2sqlem2  15667  2sqlem10  15677  vtxvalprc  15727  iedgvalprc  15728  upgrex  15774  bj-pm2.18st  15825  bj-dcstab  15831  decidi  15870  sumdc2  15874  bj-charfunbi  15885  bdel  15919  bdssex  15976  bj-indind  16006  findset  16019  nninfall  16087  trirec0  16124  neap0mkv  16149