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  2833  gencbvex  2848  gencbval  2850  vtoclgf  2860  vtoclg1f  2861  pm13.183  2942  elrabi  2957  eueq2dc  2977  eueq3dc  2978  mob2  2984  euxfr2dc  2989  reu3  2994  rmoim  3005  2rmorex  3010  sbcex  3038  sbcbi2  3080  ra5  3119  sseq1  3248  difdif  3330  dfss4st  3438  difindiss  3459  undif3ss  3466  dfrab3ss  3483  abvor0dc  3516  reldisj  3544  disjel  3547  inssdif0im  3560  uneqdifeqim  3578  r19.2m  3579  r19.2mOLD  3580  r19.3rm  3581  r19.9rmv  3584  rexm  3592  ralm  3596  raaanlem  3597  ifnefalse  3614  ifnotdc  3642  ifandc  3644  ifmdc  3646  nelpri  3691  nelprd  3693  prprc1  3778  difprsn2  3811  diftpsn3  3812  snsssn  3842  preqr2  3850  preq12b  3851  opthpr  3853  prneimg  3855  oprcl  3884  pwprss  3887  intmin4  3954  uniintabim  3963  dfiin2g  4001  iinss2  4021  iundif2ss  4034  disjnim  4076  disjnims  4077  invdisj  4079  disjiun  4081  brne0  4136  brm  4137  trel  4192  trss  4194  ssex  4224  bnd2  4261  abssexg  4270  exmidexmid  4284  rext  4305  unipw  4307  euabex  4315  mss  4316  exss  4317  copsexg  4334  opelopabsb  4352  pwssunim  4379  epelg  4385  sowlin  4415  sotritric  4419  elsuci  4498  sucprc  4507  reusv3  4555  ordon  4582  onsucmin  4603  onsucelsucr  4604  unon  4607  onsucelsucexmid  4626  setind  4635  setind2  4636  sucprcreg  4645  en2lp  4650  eunex  4657  ordsoexmid  4658  ordpwsucss  4663  tfi  4678  peano1  4690  peano2  4691  find  4695  0nelelxp  4752  opelxp  4753  elvvuni  4788  optocl  4800  ralxpf  4874  rexxpf  4875  relop  4878  breldm  4933  reldmm  4948  dmxpm  4950  elreldm  4956  dmrnssfld  4993  dmcosseq  5002  resabs1  5040  resima2  5045  issref  5117  asymref  5120  xpidtr  5125  trin2  5126  poirr2  5127  xpmlem  5155  dmxpss  5165  xp11m  5173  cnveqb  5190  dfco2a  5235  cores2  5247  coi2  5251  relcnvtr  5254  relresfld  5264  relcnvexb  5274  cnviinm  5276  iotauni  5297  iota1  5299  iota4  5304  iotam  5316  dffun8  5352  fununfun  5370  funcnvsn  5372  imadif  5407  imainlem  5408  fcoi1  5514  fcoi2  5515  f0rn0  5528  f1ocnv  5593  f1ocnvb  5594  fun11iun  5601  ffoss  5612  f1o00  5616  fo00  5617  relelfvdm  5667  nfvres  5671  nfunsn  5672  ssimaex  5703  fvmptss2  5717  fvmptssdm  5727  unpreima  5768  respreima  5771  elrnrexdm  5782  elrnrexdmb  5783  rexrnmpt  5786  dffo4  5791  rnmptss  5804  funiun  5824  funopdmsn  5829  fvpr1  5853  fvpr2  5854  elunirn  5902  f1veqaeq  5905  isores1  5950  iotaexel  5971  riotauni  5973  riotacl2  5981  riota1  5986  riota1a  5987  snriota  5998  eusvobj2  5999  acexmidlema  6004  acexmidlemb  6005  acexmidlem2  6010  oprabid  6045  0neqopab  6061  brabvv  6062  1stval2  6313  2ndval2  6314  xp1st  6323  xp2nd  6324  unielxp  6332  releldm2  6343  cnvf1o  6385  fo2ndf  6387  poxp  6392  reldmtpos  6414  dftpos4  6424  tpostpos  6425  tpostpos2  6426  iunon  6445  smoel  6461  tfrlem4  6474  tfrlem7  6478  tfrlem8  6479  tfrlem9  6480  nnaord  6672  ecexr  6702  swoord1  6726  swoord2  6727  0er  6731  mapprc  6816  mapsnconst  6858  ixpf  6884  mptelixpg  6898  idssen  6945  ener  6948  en0  6964  en1  6968  en1bg  6969  2dom  6975  modom  6989  enm  6999  xpsnen  7000  ssenen  7032  snnen2og  7040  php5dom  7044  phpm  7047  findcard  7070  findcard2  7071  findcard2s  7072  unfiexmid  7103  fiintim  7116  fidcenumlemim  7142  sbthlem1  7147  fiss  7167  djuexb  7234  djuss  7260  eldju2ndl  7262  eldju2ndr  7263  ctssdclemr  7302  exmidlpo  7333  finnum  7378  ficardon  7384  exmidfodomrlemim  7402  acnrcl  7406  3nsssucpw1  7444  indpi  7552  subhalfnqq  7624  archnqq  7627  enq0sym  7642  nqnq0pi  7648  nqnq0  7651  mulnnnq0  7660  prml  7687  prmu  7688  prssnql  7689  prssnqu  7690  prcdnql  7694  prcunqu  7695  prltlu  7697  prnmaxl  7698  prnminu  7699  prloc  7701  prdisj  7702  addcanprg  7826  recexprlemopl  7835  recexprlemopu  7837  cauappcvgprlemladdfu  7864  caucvgprlemladdfu  7887  recexgt0sr  7983  renfdisj  8229  axsuploc  8242  negf1o  8551  recexre  8748  apsqgt0  8771  apreim  8773  aprcl  8816  recexaplem2  8822  rerecclap  8900  nn0ge0  9417  elnnnn0b  9436  xnn0xr  9460  xnn0nemnf  9466  xnn0nnn0pnf  9468  znegcl  9500  zeo  9575  nn0ind  9584  nn0ind-raph  9587  uzn0  9762  eluzaddi  9773  eluzsubi  9774  uznn0sub  9778  uz3m2nn  9797  uznnssnn  9801  uz2m1nn  9829  uz2mulcl  9832  indstr2  9833  qmulz  9847  qre  9849  qnegcl  9860  qreccl  9866  rphalflt  9908  nn0ledivnn  9992  xrltnr  10004  nltpnft  10039  ngtmnft  10042  xrrebnd  10044  xnegcl  10057  xnegneg  10058  xltnegi  10060  xrpnfdc  10067  xrmnfdc  10068  xnegid  10084  xaddid1  10087  xnn0lenn0nn0  10090  xnn0xadd0  10092  xposdif  10107  elioore  10137  elfzuz2  10254  uzsubsubfz  10272  fzdisj  10277  fzmmmeqm  10283  elfz0ubfz0  10350  elfz0fzfz0  10351  fz0fzelfz0  10352  fz0fzdiffz0  10355  elfzmlbp  10357  difelfzle  10359  difelfznle  10360  nn0disj  10363  2ffzeq  10366  fzo1fzo0n0  10412  elfzo0z  10413  elfzo0le  10414  fzonmapblen  10416  fzofzim  10417  elfzodifsumelfzo  10436  elfzonlteqm1  10445  fzonn0p1p1  10448  elfzom1p1elfzo  10449  ssfzo12bi  10460  ubmelm1fzo  10461  fzind2  10475  subfzo0  10478  infssuzcldc  10485  rebtwn2z  10504  fldiv4p1lem1div2  10555  fldiv4lem1div2  10557  flqeqceilz  10570  zmodidfzoimp  10606  modfzo0difsn  10647  nnsinds  10697  nn0sinds  10698  expcl2lemap  10803  qexpclz  10812  zzlesq  10960  facp1  10982  facnn2  10986  faclbnd3  10995  bcn1  11010  hashfz0  11079  wrdf  11109  swrdswrdlem  11275  swrdswrd  11276  swrdccatin1  11296  pfxccatin12lem2a  11298  pfxccatin12lem1  11299  swrdccatin2  11300  pfxccatin12lem2  11302  pfxccatin12lem3  11303  pfxccatin12  11304  pfxccat3  11305  swrdccat  11306  swrdccat3blem  11310  cvg1nlemres  11536  rexanuz  11539  fclim  11845  climmo  11849  iser3shft  11897  fsumsplitsn  11961  fsum2dlemstep  11985  fisumcom2  11989  arisum  12049  arisum2  12050  prodmodc  12129  fprodfac  12166  fprod2dlemstep  12173  fprodcom2fi  12177  fprodsplitsn  12184  eftlub  12241  ef01bndlem  12307  sin01gt0  12313  cos01gt0  12314  sin02gt0  12315  dvdsdivcl  12401  addmodlteqALT  12410  odd2np1  12424  oddge22np1  12432  m1expe  12450  nn0enne  12453  nn0o1gt2  12456  nno  12457  ndvdsadd  12482  dfgcd2  12575  mulgcd  12577  algfx  12614  prmind2  12682  prm2orodd  12688  prmgt1  12694  oddprmgt2  12696  dfphi2  12782  nnnn0modprm0  12818  prm23lt5  12826  pythagtriplem2  12829  pcz  12895  dvdsprmpweqnn  12899  oddprmdvds  12917  prmunb  12925  4sqlem4  12955  4sqlem19  12972  evenennn  13004  fngsum  13461  igsumvalx  13462  dfgrp3me  13673  mulgnn0gsum  13705  rngdi  13943  rngdir  13944  dvdsrcl2  14103  unitinvcl  14127  unitinvinv  14128  unitlinv  14130  unitrinv  14131  rmodislmodlem  14354  rmodislmod  14355  zrhval  14621  psrbagf  14674  distop  14799  ntrss  14833  ssntr  14836  lmrcl  14906  txuni2  14970  txcn  14989  hmeocnvb  15032  xmetunirn  15072  blssioo  15267  divcnap  15279  cdivcncfap  15318  dedekindeulemlub  15334  dedekindicclemlub  15343  dvexp2  15426  elply2  15449  plyco  15473  pilem3  15497  sincosq1sgn  15540  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  sinq12gt0  15544  fsumdvdsmul  15705  zabsle1  15718  lgsdir2lem4  15750  gausslemma2dlem0f  15773  gausslemma2dlem1a  15777  gausslemma2dlem2  15781  gausslemma2dlem3  15782  gausslemma2dlem4  15783  2lgslem1a1  15805  2lgslem3  15820  2lgsoddprmlem3  15830  2lgsoddprm  15832  2sqlem2  15834  2sqlem10  15844  vtxvalprc  15896  iedgvalprc  15897  upgrex  15944  umgredg  15984  ausgrusgrben  16007  usgruspgrben  16025  usgrislfuspgrdom  16029  uhgr2edg  16045  uspgredg2v  16060  griedg0ssusgr  16090  wlkv  16123  wlk1walkdom  16156  trlsv  16179  trlf1  16183  clwwlk1loop  16194  clwwlkext2edg  16217  umgr2cwwkdifex  16220  clwwlknonex2lem2  16233  clwwlknonex2e  16235  eupthv  16241  bj-pm2.18st  16282  bj-dcstab  16288  decidi  16327  sumdc2  16331  bj-charfunbi  16342  bdel  16376  bdssex  16433  bj-indind  16463  findset  16476  nninfall  16547  trirec0  16584  neap0mkv  16609