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  590  sylnbi  682  dcim  846  notnotrdc  848  condcOLD  859  pm2.61ddc  866  pm5.18dc  888  pm2.25dc  898  pm2.85dc  910  pm5.12dc  915  pm5.14dc  916  pm5.55dc  918  peircedc  919  pm5.54dc  923  dcand  938  dcor  941  pm5.62dc  951  pm5.63dc  952  pm4.83dc  957  ifp2  986  ifpor  993  1fpid3  1000  3simpb  1019  3simpc  1020  3imp  1217  3com12  1231  3com13  1232  syl3anb  1314  xoranor  1419  xorbin  1426  xordc1  1435  biassdc  1437  nfr  1564  nfand  1614  19.21t  1628  19.30dc  1673  exintrbi  1679  19.9t  1688  nfnt  1702  equveli  1805  exdistrfor  1846  sbcof2  1856  sbidm  1897  sbi1v  1938  sbalyz  2050  sbal1yz  2052  nfsb4t  2065  euex  2107  eumo0  2108  mor  2120  exmodc  2128  mo3h  2131  mopick  2156  moexexdc  2162  euexex  2163  2euex  2165  exists2  2175  eqcoms  2232  eleq2s  2324  nfcr  2364  necon3ai  2449  rexnalim  2519  dfrex2dc  2521  rexex  2576  rsp  2577  ralim  2589  rexim  2624  r19.32r  2677  r19.44av  2690  r19.45av  2691  gencl  2832  gencbvex  2847  gencbval  2849  vtoclgf  2859  vtoclg1f  2860  pm13.183  2941  elrabi  2956  eueq2dc  2976  eueq3dc  2977  mob2  2983  euxfr2dc  2988  reu3  2993  rmoim  3004  2rmorex  3009  sbcex  3037  sbcbi2  3079  ra5  3118  sseq1  3247  difdif  3329  dfss4st  3437  difindiss  3458  undif3ss  3465  dfrab3ss  3482  abvor0dc  3515  reldisj  3543  disjel  3546  inssdif0im  3559  uneqdifeqim  3577  r19.2m  3578  r19.2mOLD  3579  r19.3rm  3580  r19.9rmv  3583  rexm  3591  ralm  3595  raaanlem  3596  ifnefalse  3613  ifnotdc  3641  ifandc  3643  ifmdc  3645  nelpri  3690  nelprd  3692  prprc1  3774  difprsn2  3807  diftpsn3  3808  snsssn  3838  preqr2  3846  preq12b  3847  opthpr  3849  prneimg  3851  oprcl  3880  pwprss  3883  intmin4  3950  uniintabim  3959  dfiin2g  3997  iinss2  4017  iundif2ss  4030  disjnim  4072  disjnims  4073  invdisj  4075  disjiun  4077  brne0  4132  brm  4133  trel  4188  trss  4190  ssex  4220  bnd2  4256  abssexg  4265  exmidexmid  4279  rext  4300  unipw  4302  euabex  4310  mss  4311  exss  4312  copsexg  4329  opelopabsb  4347  pwssunim  4374  epelg  4380  sowlin  4410  sotritric  4414  elsuci  4493  sucprc  4502  reusv3  4550  ordon  4577  onsucmin  4598  onsucelsucr  4599  unon  4602  onsucelsucexmid  4621  setind  4630  setind2  4631  sucprcreg  4640  en2lp  4645  eunex  4652  ordsoexmid  4653  ordpwsucss  4658  tfi  4673  peano1  4685  peano2  4686  find  4690  0nelelxp  4747  opelxp  4748  elvvuni  4782  optocl  4794  ralxpf  4867  rexxpf  4868  relop  4871  breldm  4926  reldmm  4941  dmxpm  4943  elreldm  4949  dmrnssfld  4986  dmcosseq  4995  resabs1  5033  resima2  5038  issref  5110  asymref  5113  xpidtr  5118  trin2  5119  poirr2  5120  xpmlem  5148  dmxpss  5158  xp11m  5166  cnveqb  5183  dfco2a  5228  cores2  5240  coi2  5244  relcnvtr  5247  relresfld  5257  relcnvexb  5267  cnviinm  5269  iotauni  5290  iota1  5292  iota4  5297  iotam  5309  dffun8  5345  fununfun  5363  funcnvsn  5365  imadif  5400  imainlem  5401  fcoi1  5505  fcoi2  5506  f0rn0  5519  f1ocnv  5584  f1ocnvb  5585  fun11iun  5592  ffoss  5603  f1o00  5607  fo00  5608  relelfvdm  5658  nfvres  5662  nfunsn  5663  ssimaex  5694  fvmptss2  5708  fvmptssdm  5718  unpreima  5759  respreima  5762  elrnrexdm  5773  elrnrexdmb  5774  rexrnmpt  5777  dffo4  5782  rnmptss  5795  funiun  5815  funopdmsn  5818  fvpr1  5842  fvpr2  5843  elunirn  5889  f1veqaeq  5892  isores1  5937  iotaexel  5958  riotauni  5960  riotacl2  5968  riota1  5973  riota1a  5974  snriota  5985  eusvobj2  5986  acexmidlema  5991  acexmidlemb  5992  acexmidlem2  5997  oprabid  6032  0neqopab  6048  brabvv  6049  1stval2  6299  2ndval2  6300  xp1st  6309  xp2nd  6310  unielxp  6318  releldm2  6329  cnvf1o  6369  fo2ndf  6371  poxp  6376  reldmtpos  6397  dftpos4  6407  tpostpos  6408  tpostpos2  6409  iunon  6428  smoel  6444  tfrlem4  6457  tfrlem7  6461  tfrlem8  6462  tfrlem9  6463  nnaord  6653  ecexr  6683  swoord1  6707  swoord2  6708  0er  6712  mapprc  6797  mapsnconst  6839  ixpf  6865  mptelixpg  6879  idssen  6926  ener  6929  en0  6945  en1  6949  en1bg  6950  2dom  6956  enm  6975  xpsnen  6976  ssenen  7008  snnen2og  7016  php5dom  7020  phpm  7023  findcard  7046  findcard2  7047  findcard2s  7048  unfiexmid  7076  fiintim  7089  fidcenumlemim  7115  sbthlem1  7120  fiss  7140  djuexb  7207  djuss  7233  eldju2ndl  7235  eldju2ndr  7236  ctssdclemr  7275  exmidlpo  7306  finnum  7351  ficardon  7357  exmidfodomrlemim  7375  acnrcl  7379  3nsssucpw1  7417  indpi  7525  subhalfnqq  7597  archnqq  7600  enq0sym  7615  nqnq0pi  7621  nqnq0  7624  mulnnnq0  7633  prml  7660  prmu  7661  prssnql  7662  prssnqu  7663  prcdnql  7667  prcunqu  7668  prltlu  7670  prnmaxl  7671  prnminu  7672  prloc  7674  prdisj  7675  addcanprg  7799  recexprlemopl  7808  recexprlemopu  7810  cauappcvgprlemladdfu  7837  caucvgprlemladdfu  7860  recexgt0sr  7956  renfdisj  8202  axsuploc  8215  negf1o  8524  recexre  8721  apsqgt0  8744  apreim  8746  aprcl  8789  recexaplem2  8795  rerecclap  8873  nn0ge0  9390  elnnnn0b  9409  xnn0xr  9433  xnn0nemnf  9439  xnn0nnn0pnf  9441  znegcl  9473  zeo  9548  nn0ind  9557  nn0ind-raph  9560  uzn0  9734  eluzaddi  9745  eluzsubi  9746  uznn0sub  9750  uz3m2nn  9764  uznnssnn  9768  uz2m1nn  9796  uz2mulcl  9799  indstr2  9800  qmulz  9814  qre  9816  qnegcl  9827  qreccl  9833  rphalflt  9875  nn0ledivnn  9959  xrltnr  9971  nltpnft  10006  ngtmnft  10009  xrrebnd  10011  xnegcl  10024  xnegneg  10025  xltnegi  10027  xrpnfdc  10034  xrmnfdc  10035  xnegid  10051  xaddid1  10054  xnn0lenn0nn0  10057  xnn0xadd0  10059  xposdif  10074  elioore  10104  elfzuz2  10221  uzsubsubfz  10239  fzdisj  10244  fzmmmeqm  10250  elfz0ubfz0  10317  elfz0fzfz0  10318  fz0fzelfz0  10319  fz0fzdiffz0  10322  elfzmlbp  10324  difelfzle  10326  difelfznle  10327  nn0disj  10330  2ffzeq  10333  fzo1fzo0n0  10379  elfzo0z  10380  elfzo0le  10381  fzonmapblen  10383  fzofzim  10384  elfzodifsumelfzo  10402  elfzonlteqm1  10411  fzonn0p1p1  10414  elfzom1p1elfzo  10415  ssfzo12bi  10426  ubmelm1fzo  10427  fzind2  10440  subfzo0  10443  infssuzcldc  10450  rebtwn2z  10469  fldiv4p1lem1div2  10520  fldiv4lem1div2  10522  flqeqceilz  10535  zmodidfzoimp  10571  modfzo0difsn  10612  nnsinds  10662  nn0sinds  10663  expcl2lemap  10768  qexpclz  10777  zzlesq  10925  facp1  10947  facnn2  10951  faclbnd3  10960  bcn1  10975  hashfz0  11042  wrdf  11072  swrdswrdlem  11231  swrdswrd  11232  swrdccatin1  11252  pfxccatin12lem2a  11254  pfxccatin12lem1  11255  swrdccatin2  11256  pfxccatin12lem2  11258  pfxccatin12lem3  11259  pfxccatin12  11260  pfxccat3  11261  swrdccat  11262  swrdccat3blem  11266  cvg1nlemres  11491  rexanuz  11494  fclim  11800  climmo  11804  iser3shft  11852  fsumsplitsn  11916  fsum2dlemstep  11940  fisumcom2  11944  arisum  12004  arisum2  12005  prodmodc  12084  fprodfac  12121  fprod2dlemstep  12128  fprodcom2fi  12132  fprodsplitsn  12139  eftlub  12196  ef01bndlem  12262  sin01gt0  12268  cos01gt0  12269  sin02gt0  12270  dvdsdivcl  12356  addmodlteqALT  12365  odd2np1  12379  oddge22np1  12387  m1expe  12405  nn0enne  12408  nn0o1gt2  12411  nno  12412  ndvdsadd  12437  dfgcd2  12530  mulgcd  12532  algfx  12569  prmind2  12637  prm2orodd  12643  prmgt1  12649  oddprmgt2  12651  dfphi2  12737  nnnn0modprm0  12773  prm23lt5  12781  pythagtriplem2  12784  pcz  12850  dvdsprmpweqnn  12854  oddprmdvds  12872  prmunb  12880  4sqlem4  12910  4sqlem19  12927  evenennn  12959  fngsum  13416  igsumvalx  13417  dfgrp3me  13628  mulgnn0gsum  13660  rngdi  13898  rngdir  13899  dvdsrcl2  14057  unitinvcl  14081  unitinvinv  14082  unitlinv  14084  unitrinv  14085  rmodislmodlem  14308  rmodislmod  14309  zrhval  14575  psrbagf  14628  distop  14753  ntrss  14787  ssntr  14790  lmrcl  14859  lmreltop  14861  txuni2  14924  txcn  14943  hmeocnvb  14986  xmetunirn  15026  blssioo  15221  divcnap  15233  cdivcncfap  15272  dedekindeulemlub  15288  dedekindicclemlub  15297  dvexp2  15380  elply2  15403  plyco  15427  pilem3  15451  sincosq1sgn  15494  sincosq2sgn  15495  sincosq3sgn  15496  sincosq4sgn  15497  sinq12gt0  15498  fsumdvdsmul  15659  zabsle1  15672  lgsdir2lem4  15704  gausslemma2dlem0f  15727  gausslemma2dlem1a  15731  gausslemma2dlem2  15735  gausslemma2dlem3  15736  gausslemma2dlem4  15737  2lgslem1a1  15759  2lgslem3  15774  2lgsoddprmlem3  15784  2lgsoddprm  15786  2sqlem2  15788  2sqlem10  15798  vtxvalprc  15850  iedgvalprc  15851  upgrex  15897  umgredg  15937  ausgrusgrben  15960  usgruspgrben  15978  usgrislfuspgrdom  15982  uhgr2edg  15998  uspgredg2v  16013  bj-pm2.18st  16072  bj-dcstab  16078  decidi  16117  sumdc2  16121  bj-charfunbi  16132  bdel  16166  bdssex  16223  bj-indind  16253  findset  16266  nninfall  16334  trirec0  16371  neap0mkv  16396