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  567  an32s  570  an4s  592  sylnbi  684  dcim  848  notnotrdc  850  condcOLD  861  pm2.61ddc  868  pm5.18dc  890  pm2.25dc  900  pm2.85dc  912  pm5.12dc  917  pm5.14dc  918  pm5.55dc  920  peircedc  921  pm5.54dc  925  dcand  940  dcor  943  pm5.62dc  953  pm5.63dc  954  pm4.83dc  959  ifp2  988  ifpor  995  1fpid3  1002  3simpb  1021  3simpc  1022  3imp  1219  3com12  1233  3com13  1234  syl3anb  1316  xoranor  1421  xorbin  1428  xordc1  1437  biassdc  1439  nfr  1566  nfand  1616  19.21t  1630  19.30dc  1675  exintrbi  1681  19.9t  1690  nfnt  1704  equveli  1807  exdistrfor  1848  sbcof2  1858  sbidm  1899  sbi1v  1940  sbalyz  2052  sbal1yz  2054  nfsb4t  2067  euex  2109  eumo0  2110  mor  2122  exmodc  2130  mo3h  2133  mopick  2158  moexexdc  2164  euexex  2165  2euex  2167  exists2  2177  eqcoms  2234  eleq2s  2326  nfcr  2366  necon3ai  2451  rexnalim  2521  dfrex2dc  2523  rexex  2578  rsp  2579  ralim  2591  rexim  2626  r19.32r  2679  r19.44av  2692  r19.45av  2693  gencl  2835  gencbvex  2850  gencbval  2852  vtoclgf  2862  vtoclg1f  2863  pm13.183  2944  elrabi  2959  eueq2dc  2979  eueq3dc  2980  mob2  2986  euxfr2dc  2991  reu3  2996  rmoim  3007  2rmorex  3012  sbcex  3040  sbcbi2  3082  ra5  3121  sseq1  3250  difdif  3332  dfss4st  3440  difindiss  3461  undif3ss  3468  dfrab3ss  3485  abvor0dc  3518  reldisj  3546  disjel  3549  inssdif0im  3562  uneqdifeqim  3580  r19.2m  3581  r19.2mOLD  3582  r19.3rm  3583  r19.9rmv  3586  rexm  3594  ralm  3598  raaanlem  3599  ifnefalse  3616  ifnotdc  3644  ifandc  3646  ifmdc  3648  nelpri  3693  nelprd  3695  prprc1  3780  difprsn2  3813  diftpsn3  3814  snsssn  3844  preqr2  3852  preq12b  3853  opthpr  3855  prneimg  3857  oprcl  3886  pwprss  3889  intmin4  3956  uniintabim  3965  dfiin2g  4003  iinss2  4023  iundif2ss  4036  disjnim  4078  disjnims  4079  invdisj  4081  disjiun  4083  brne0  4138  brm  4139  trel  4194  trss  4196  ssex  4226  bnd2  4263  abssexg  4272  exmidexmid  4286  rext  4307  unipw  4309  euabex  4317  mss  4318  exss  4319  copsexg  4336  opelopabsb  4354  pwssunim  4381  epelg  4387  sowlin  4417  sotritric  4421  elsuci  4500  sucprc  4509  reusv3  4557  ordon  4584  onsucmin  4605  onsucelsucr  4606  unon  4609  onsucelsucexmid  4628  setind  4637  setind2  4638  sucprcreg  4647  en2lp  4652  eunex  4659  ordsoexmid  4660  ordpwsucss  4665  tfi  4680  peano1  4692  peano2  4693  find  4697  0nelelxp  4754  opelxp  4755  elvvuni  4790  optocl  4802  ralxpf  4876  rexxpf  4877  relop  4880  breldm  4935  reldmm  4950  dmxpm  4952  elreldm  4958  dmrnssfld  4995  dmcosseq  5004  resabs1  5042  resima2  5047  issref  5119  asymref  5122  xpidtr  5127  trin2  5128  poirr2  5129  xpmlem  5157  dmxpss  5167  xp11m  5175  cnveqb  5192  dfco2a  5237  cores2  5249  coi2  5253  relcnvtr  5256  relresfld  5266  relcnvexb  5276  cnviinm  5278  iotauni  5299  iota1  5301  iota4  5306  iotam  5318  dffun8  5354  fununfun  5373  funcnvsn  5375  imadif  5410  imainlem  5411  fcoi1  5517  fcoi2  5518  f0rn0  5531  f1ocnv  5596  f1ocnvb  5597  fun11iun  5604  ffoss  5616  f1o00  5620  fo00  5621  relelfvdm  5671  nfvres  5675  nfunsn  5676  ssimaex  5707  fvmptss2  5721  fvmptssdm  5731  unpreima  5772  respreima  5775  elrnrexdm  5786  elrnrexdmb  5787  rexrnmpt  5790  dffo4  5795  rnmptss  5808  funiun  5829  funopdmsn  5834  fvpr1  5858  fvpr2  5859  elunirn  5907  f1veqaeq  5910  isores1  5955  iotaexel  5976  riotauni  5978  riotacl2  5986  riota1  5991  riota1a  5992  snriota  6003  eusvobj2  6004  acexmidlema  6009  acexmidlemb  6010  acexmidlem2  6015  oprabid  6050  0neqopab  6066  brabvv  6067  1stval2  6318  2ndval2  6319  xp1st  6328  xp2nd  6329  unielxp  6337  releldm2  6348  cnvf1o  6390  fo2ndf  6392  poxp  6397  reldmtpos  6419  dftpos4  6429  tpostpos  6430  tpostpos2  6431  iunon  6450  smoel  6466  tfrlem4  6479  tfrlem7  6483  tfrlem8  6484  tfrlem9  6485  nnaord  6677  ecexr  6707  swoord1  6731  swoord2  6732  0er  6736  mapprc  6821  mapsnconst  6863  ixpf  6889  mptelixpg  6903  idssen  6950  ener  6953  en0  6969  en1  6973  en1bg  6974  2dom  6980  modom  6994  enm  7004  xpsnen  7005  ssenen  7037  snnen2og  7045  php5dom  7049  phpm  7052  findcard  7077  findcard2  7078  findcard2s  7079  unfiexmid  7110  fiintim  7123  fidcenumlemim  7151  sbthlem1  7156  fiss  7176  djuexb  7243  djuss  7269  eldju2ndl  7271  eldju2ndr  7272  ctssdclemr  7311  exmidlpo  7342  finnum  7387  ficardon  7393  exmidfodomrlemim  7412  acnrcl  7416  3nsssucpw1  7454  indpi  7562  subhalfnqq  7634  archnqq  7637  enq0sym  7652  nqnq0pi  7658  nqnq0  7661  mulnnnq0  7670  prml  7697  prmu  7698  prssnql  7699  prssnqu  7700  prcdnql  7704  prcunqu  7705  prltlu  7707  prnmaxl  7708  prnminu  7709  prloc  7711  prdisj  7712  addcanprg  7836  recexprlemopl  7845  recexprlemopu  7847  cauappcvgprlemladdfu  7874  caucvgprlemladdfu  7897  recexgt0sr  7993  renfdisj  8239  axsuploc  8252  negf1o  8561  recexre  8758  apsqgt0  8781  apreim  8783  aprcl  8826  recexaplem2  8832  rerecclap  8910  nn0ge0  9427  elnnnn0b  9446  xnn0xr  9470  xnn0nemnf  9476  xnn0nnn0pnf  9478  znegcl  9510  zeo  9585  nn0ind  9594  nn0ind-raph  9597  uzn0  9772  eluzaddi  9783  eluzsubi  9784  uznn0sub  9788  uz3m2nn  9807  uznnssnn  9811  uz2m1nn  9839  uz2mulcl  9842  indstr2  9843  qmulz  9857  qre  9859  qnegcl  9870  qreccl  9876  rphalflt  9918  nn0ledivnn  10002  xrltnr  10014  nltpnft  10049  ngtmnft  10052  xrrebnd  10054  xnegcl  10067  xnegneg  10068  xltnegi  10070  xrpnfdc  10077  xrmnfdc  10078  xnegid  10094  xaddid1  10097  xnn0lenn0nn0  10100  xnn0xadd0  10102  xposdif  10117  elioore  10147  elfzuz2  10264  uzsubsubfz  10282  fzdisj  10287  fzmmmeqm  10293  elfz0ubfz0  10360  elfz0fzfz0  10361  fz0fzelfz0  10362  fz0fzdiffz0  10365  elfzmlbp  10367  difelfzle  10369  difelfznle  10370  nn0disj  10373  2ffzeq  10376  fzo1fzo0n0  10423  elfzo0z  10424  elfzo0le  10425  fzonmapblen  10427  fzofzim  10428  elfzodifsumelfzo  10447  elfzonlteqm1  10456  fzonn0p1p1  10459  elfzom1p1elfzo  10460  ssfzo12bi  10471  ubmelm1fzo  10472  fzind2  10486  subfzo0  10489  infssuzcldc  10496  rebtwn2z  10515  fldiv4p1lem1div2  10566  fldiv4lem1div2  10568  flqeqceilz  10581  zmodidfzoimp  10617  modfzo0difsn  10658  nnsinds  10708  nn0sinds  10709  expcl2lemap  10814  qexpclz  10823  zzlesq  10971  facp1  10993  facnn2  10997  faclbnd3  11006  bcn1  11021  hashfz0  11090  wrdf  11123  swrdswrdlem  11289  swrdswrd  11290  swrdccatin1  11310  pfxccatin12lem2a  11312  pfxccatin12lem1  11313  swrdccatin2  11314  pfxccatin12lem2  11316  pfxccatin12lem3  11317  pfxccatin12  11318  pfxccat3  11319  swrdccat  11320  swrdccat3blem  11324  cvg1nlemres  11550  rexanuz  11553  fclim  11859  climmo  11863  iser3shft  11911  fsumsplitsn  11976  fsum2dlemstep  12000  fisumcom2  12004  arisum  12064  arisum2  12065  prodmodc  12144  fprodfac  12181  fprod2dlemstep  12188  fprodcom2fi  12192  fprodsplitsn  12199  eftlub  12256  ef01bndlem  12322  sin01gt0  12328  cos01gt0  12329  sin02gt0  12330  dvdsdivcl  12416  addmodlteqALT  12425  odd2np1  12439  oddge22np1  12447  m1expe  12465  nn0enne  12468  nn0o1gt2  12471  nno  12472  ndvdsadd  12497  dfgcd2  12590  mulgcd  12592  algfx  12629  prmind2  12697  prm2orodd  12703  prmgt1  12709  oddprmgt2  12711  dfphi2  12797  nnnn0modprm0  12833  prm23lt5  12841  pythagtriplem2  12844  pcz  12910  dvdsprmpweqnn  12914  oddprmdvds  12932  prmunb  12940  4sqlem4  12970  4sqlem19  12987  evenennn  13019  fngsum  13476  igsumvalx  13477  dfgrp3me  13688  mulgnn0gsum  13720  rngdi  13959  rngdir  13960  dvdsrcl2  14119  unitinvcl  14143  unitinvinv  14144  unitlinv  14146  unitrinv  14147  rmodislmodlem  14370  rmodislmod  14371  zrhval  14637  psrbagf  14690  distop  14815  ntrss  14849  ssntr  14852  lmrcl  14922  txuni2  14986  txcn  15005  hmeocnvb  15048  xmetunirn  15088  blssioo  15283  divcnap  15295  cdivcncfap  15334  dedekindeulemlub  15350  dedekindicclemlub  15359  dvexp2  15442  elply2  15465  plyco  15489  pilem3  15513  sincosq1sgn  15556  sincosq2sgn  15557  sincosq3sgn  15558  sincosq4sgn  15559  sinq12gt0  15560  fsumdvdsmul  15721  zabsle1  15734  lgsdir2lem4  15766  gausslemma2dlem0f  15789  gausslemma2dlem1a  15793  gausslemma2dlem2  15797  gausslemma2dlem3  15798  gausslemma2dlem4  15799  2lgslem1a1  15821  2lgslem3  15836  2lgsoddprmlem3  15846  2lgsoddprm  15848  2sqlem2  15850  2sqlem10  15860  vtxvalprc  15912  iedgvalprc  15913  upgrex  15960  umgredg  16002  ausgrusgrben  16025  usgruspgrben  16043  usgrislfuspgrdom  16047  uhgr2edg  16063  uspgredg2v  16078  griedg0ssusgr  16108  subusgr  16132  wlkv  16183  wlk1walkdom  16216  trlsv  16241  trlf1  16245  clwwlk1loop  16256  clwwlkext2edg  16279  umgr2cwwkdifex  16282  clwwlknonex2lem2  16295  clwwlknonex2e  16297  eupthv  16303  eupth2lem3lem4fi  16330  bj-pm2.18st  16372  bj-dcstab  16378  decidi  16417  sumdc2  16421  bj-charfunbi  16432  bdel  16466  bdssex  16523  bj-indind  16553  findset  16566  nninfall  16637  trirec0  16674  neap0mkv  16700