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  679  dcim  842  notnotrdc  844  condcOLD  855  pm2.61ddc  862  pm5.18dc  884  pm2.25dc  894  pm2.85dc  906  pm5.12dc  911  pm5.14dc  912  pm5.55dc  914  peircedc  915  pm5.54dc  919  dcand  934  dcor  937  pm5.62dc  947  pm5.63dc  948  pm4.83dc  953  3simpb  997  3simpc  998  3imp  1195  3com12  1209  3com13  1210  syl3anb  1292  xoranor  1388  xorbin  1395  xordc1  1404  biassdc  1406  nfr  1529  nfand  1579  19.21t  1593  19.30dc  1638  exintrbi  1644  19.9t  1653  nfnt  1667  equveli  1770  exdistrfor  1811  sbcof2  1821  sbidm  1862  sbi1v  1903  sbalyz  2015  sbal1yz  2017  nfsb4t  2030  euex  2072  eumo0  2073  mor  2084  exmodc  2092  mo3h  2095  mopick  2120  moexexdc  2126  euexex  2127  2euex  2129  exists2  2139  eqcoms  2196  eleq2s  2288  nfcr  2328  necon3ai  2413  rexnalim  2483  dfrex2dc  2485  rexex  2540  rsp  2541  ralim  2553  rexim  2588  r19.32r  2640  r19.44av  2653  r19.45av  2654  gencl  2792  gencbvex  2806  gencbval  2808  vtoclgf  2818  vtoclg1f  2819  pm13.183  2898  elrabi  2913  eueq2dc  2933  eueq3dc  2934  mob2  2940  euxfr2dc  2945  reu3  2950  rmoim  2961  2rmorex  2966  sbcex  2994  sbcbi2  3036  ra5  3074  sseq1  3202  difdif  3284  dfss4st  3392  difindiss  3413  undif3ss  3420  dfrab3ss  3437  abvor0dc  3470  reldisj  3498  disjel  3501  inssdif0im  3514  uneqdifeqim  3532  r19.2m  3533  r19.2mOLD  3534  r19.3rm  3535  r19.9rmv  3538  rexm  3546  ralm  3550  raaanlem  3551  ifnefalse  3568  ifnotdc  3594  ifandc  3595  ifmdc  3597  nelpri  3642  nelprd  3644  prprc1  3726  difprsn2  3758  diftpsn3  3759  snsssn  3787  preqr2  3795  preq12b  3796  opthpr  3798  prneimg  3800  oprcl  3828  pwprss  3831  intmin4  3898  uniintabim  3907  dfiin2g  3945  iinss2  3965  iundif2ss  3978  disjnim  4020  disjnims  4021  invdisj  4023  disjiun  4024  brne0  4078  brm  4079  trel  4134  trss  4136  ssex  4166  bnd2  4202  abssexg  4211  exmidexmid  4225  rext  4244  unipw  4246  euabex  4254  mss  4255  exss  4256  copsexg  4273  opelopabsb  4290  pwssunim  4315  epelg  4321  sowlin  4351  sotritric  4355  elsuci  4434  sucprc  4443  reusv3  4491  ordon  4518  onsucmin  4539  onsucelsucr  4540  unon  4543  onsucelsucexmid  4562  setind  4571  setind2  4572  sucprcreg  4581  en2lp  4586  eunex  4593  ordsoexmid  4594  ordpwsucss  4599  tfi  4614  peano1  4626  peano2  4627  find  4631  0nelelxp  4688  opelxp  4689  elvvuni  4723  optocl  4735  ralxpf  4808  rexxpf  4809  relop  4812  breldm  4866  dmxpm  4882  elreldm  4888  dmrnssfld  4925  dmcosseq  4933  resabs1  4971  resima2  4976  issref  5048  asymref  5051  xpidtr  5056  trin2  5057  poirr2  5058  xpmlem  5086  dmxpss  5096  xp11m  5104  cnveqb  5121  dfco2a  5166  cores2  5178  coi2  5182  relcnvtr  5185  relresfld  5195  relcnvexb  5205  cnviinm  5207  iotauni  5227  iota1  5229  iota4  5234  iotam  5246  dffun8  5282  funcnvsn  5299  imadif  5334  imainlem  5335  fcoi1  5434  fcoi2  5435  f0rn0  5448  f1ocnv  5513  f1ocnvb  5514  fun11iun  5521  ffoss  5532  f1o00  5535  fo00  5536  relelfvdm  5586  nfvres  5588  nfunsn  5589  ssimaex  5618  fvmptss2  5632  fvmptssdm  5642  unpreima  5683  respreima  5686  elrnrexdm  5697  elrnrexdmb  5698  rexrnmpt  5701  dffo4  5706  rnmptss  5719  fvpr1  5762  fvpr2  5763  elunirn  5809  f1veqaeq  5812  isores1  5857  iotaexel  5878  riotauni  5880  riotacl2  5887  riota1  5892  riota1a  5893  snriota  5903  eusvobj2  5904  acexmidlema  5909  acexmidlemb  5910  acexmidlem2  5915  oprabid  5950  0neqopab  5963  brabvv  5964  1stval2  6208  2ndval2  6209  xp1st  6218  xp2nd  6219  unielxp  6227  releldm2  6238  cnvf1o  6278  fo2ndf  6280  poxp  6285  reldmtpos  6306  dftpos4  6316  tpostpos  6317  tpostpos2  6318  iunon  6337  smoel  6353  tfrlem4  6366  tfrlem7  6370  tfrlem8  6371  tfrlem9  6372  nnaord  6562  ecexr  6592  swoord1  6616  swoord2  6617  0er  6621  mapprc  6706  mapsnconst  6748  ixpf  6774  mptelixpg  6788  idssen  6831  ener  6833  en0  6849  en1  6853  en1bg  6854  2dom  6859  enm  6874  xpsnen  6875  ssenen  6907  snnen2og  6915  php5dom  6919  phpm  6921  findcard  6944  findcard2  6945  findcard2s  6946  unfiexmid  6974  fiintim  6985  fidcenumlemim  7011  sbthlem1  7016  fiss  7036  djuexb  7103  djuss  7129  eldju2ndl  7131  eldju2ndr  7132  ctssdclemr  7171  exmidlpo  7202  finnum  7243  exmidfodomrlemim  7261  3nsssucpw1  7296  indpi  7402  subhalfnqq  7474  archnqq  7477  enq0sym  7492  nqnq0pi  7498  nqnq0  7501  mulnnnq0  7510  prml  7537  prmu  7538  prssnql  7539  prssnqu  7540  prcdnql  7544  prcunqu  7545  prltlu  7547  prnmaxl  7548  prnminu  7549  prloc  7551  prdisj  7552  addcanprg  7676  recexprlemopl  7685  recexprlemopu  7687  cauappcvgprlemladdfu  7714  caucvgprlemladdfu  7737  recexgt0sr  7833  renfdisj  8079  axsuploc  8092  negf1o  8401  recexre  8597  apsqgt0  8620  apreim  8622  aprcl  8665  recexaplem2  8671  rerecclap  8749  nn0ge0  9265  elnnnn0b  9284  xnn0xr  9308  xnn0nemnf  9314  xnn0nnn0pnf  9316  znegcl  9348  zeo  9422  nn0ind  9431  nn0ind-raph  9434  uzn0  9608  eluzaddi  9619  eluzsubi  9620  uznn0sub  9624  uz3m2nn  9638  uznnssnn  9642  uz2m1nn  9670  uz2mulcl  9673  indstr2  9674  qmulz  9688  qre  9690  qnegcl  9701  qreccl  9707  rphalflt  9749  nn0ledivnn  9833  xrltnr  9845  nltpnft  9880  ngtmnft  9883  xrrebnd  9885  xnegcl  9898  xnegneg  9899  xltnegi  9901  xrpnfdc  9908  xrmnfdc  9909  xnegid  9925  xaddid1  9928  xnn0lenn0nn0  9931  xnn0xadd0  9933  xposdif  9948  elioore  9978  elfzuz2  10095  uzsubsubfz  10113  fzdisj  10118  fzmmmeqm  10124  elfz0ubfz0  10191  elfz0fzfz0  10192  fz0fzelfz0  10193  fz0fzdiffz0  10196  elfzmlbp  10198  difelfzle  10200  difelfznle  10201  nn0disj  10204  2ffzeq  10207  fzo1fzo0n0  10250  elfzo0z  10251  elfzo0le  10252  fzonmapblen  10254  fzofzim  10255  elfzodifsumelfzo  10268  elfzonlteqm1  10277  fzonn0p1p1  10280  elfzom1p1elfzo  10281  ssfzo12bi  10292  ubmelm1fzo  10293  fzind2  10306  subfzo0  10309  rebtwn2z  10323  fldiv4p1lem1div2  10374  fldiv4lem1div2  10376  flqeqceilz  10389  zmodidfzoimp  10425  modfzo0difsn  10466  nnsinds  10516  nn0sinds  10517  expcl2lemap  10622  qexpclz  10631  zzlesq  10779  facp1  10801  facnn2  10805  faclbnd3  10814  bcn1  10829  hashfz0  10896  wrdf  10920  cvg1nlemres  11129  rexanuz  11132  fclim  11437  climmo  11441  iser3shft  11489  fsumsplitsn  11553  fsum2dlemstep  11577  fisumcom2  11581  arisum  11641  arisum2  11642  prodmodc  11721  fprodfac  11758  fprod2dlemstep  11765  fprodcom2fi  11769  fprodsplitsn  11776  eftlub  11833  ef01bndlem  11899  sin01gt0  11905  cos01gt0  11906  sin02gt0  11907  dvdsdivcl  11992  addmodlteqALT  12001  odd2np1  12014  oddge22np1  12022  m1expe  12040  nn0enne  12043  nn0o1gt2  12046  nno  12047  ndvdsadd  12072  infssuzcldc  12088  dfgcd2  12151  mulgcd  12153  algfx  12190  prmind2  12258  prm2orodd  12264  prmgt1  12270  oddprmgt2  12272  dfphi2  12358  nnnn0modprm0  12393  prm23lt5  12401  pythagtriplem2  12404  pcz  12470  dvdsprmpweqnn  12474  oddprmdvds  12492  prmunb  12500  4sqlem4  12530  4sqlem19  12547  evenennn  12550  fngsum  12971  igsumvalx  12972  dfgrp3me  13172  mulgnn0gsum  13198  rngdi  13436  rngdir  13437  dvdsrcl2  13595  unitinvcl  13619  unitinvinv  13620  unitlinv  13622  unitrinv  13623  rmodislmodlem  13846  rmodislmod  13847  zrhval  14105  psrbagf  14156  distop  14253  ntrss  14287  ssntr  14290  lmrcl  14359  lmreltop  14361  txuni2  14424  txcn  14443  hmeocnvb  14486  xmetunirn  14526  blssioo  14713  divcnap  14723  cdivcncfap  14758  dedekindeulemlub  14774  dedekindicclemlub  14783  dvexp2  14861  elply2  14881  pilem3  14918  sincosq1sgn  14961  sincosq2sgn  14962  sincosq3sgn  14963  sincosq4sgn  14964  sinq12gt0  14965  zabsle1  15115  lgsdir2lem4  15147  gausslemma2dlem0f  15170  gausslemma2dlem1a  15174  gausslemma2dlem2  15178  gausslemma2dlem3  15179  gausslemma2dlem4  15180  2lgsoddprmlem3  15199  2sqlem2  15202  2sqlem10  15212  bj-pm2.18st  15242  bj-dcstab  15248  decidi  15287  sumdc2  15291  bj-charfunbi  15303  bdel  15337  bdssex  15394  bj-indind  15424  findset  15437  nninfall  15499  trirec0  15534  neap0mkv  15559