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  3775  difprsn2  3808  diftpsn3  3809  snsssn  3839  preqr2  3847  preq12b  3848  opthpr  3850  prneimg  3852  oprcl  3881  pwprss  3884  intmin4  3951  uniintabim  3960  dfiin2g  3998  iinss2  4018  iundif2ss  4031  disjnim  4073  disjnims  4074  invdisj  4076  disjiun  4078  brne0  4133  brm  4134  trel  4189  trss  4191  ssex  4221  bnd2  4257  abssexg  4266  exmidexmid  4280  rext  4301  unipw  4303  euabex  4311  mss  4312  exss  4313  copsexg  4330  opelopabsb  4348  pwssunim  4375  epelg  4381  sowlin  4411  sotritric  4415  elsuci  4494  sucprc  4503  reusv3  4551  ordon  4578  onsucmin  4599  onsucelsucr  4600  unon  4603  onsucelsucexmid  4622  setind  4631  setind2  4632  sucprcreg  4641  en2lp  4646  eunex  4653  ordsoexmid  4654  ordpwsucss  4659  tfi  4674  peano1  4686  peano2  4687  find  4691  0nelelxp  4748  opelxp  4749  elvvuni  4783  optocl  4795  ralxpf  4868  rexxpf  4869  relop  4872  breldm  4927  reldmm  4942  dmxpm  4944  elreldm  4950  dmrnssfld  4987  dmcosseq  4996  resabs1  5034  resima2  5039  issref  5111  asymref  5114  xpidtr  5119  trin2  5120  poirr2  5121  xpmlem  5149  dmxpss  5159  xp11m  5167  cnveqb  5184  dfco2a  5229  cores2  5241  coi2  5245  relcnvtr  5248  relresfld  5258  relcnvexb  5268  cnviinm  5270  iotauni  5291  iota1  5293  iota4  5298  iotam  5310  dffun8  5346  fununfun  5364  funcnvsn  5366  imadif  5401  imainlem  5402  fcoi1  5508  fcoi2  5509  f0rn0  5522  f1ocnv  5587  f1ocnvb  5588  fun11iun  5595  ffoss  5606  f1o00  5610  fo00  5611  relelfvdm  5661  nfvres  5665  nfunsn  5666  ssimaex  5697  fvmptss2  5711  fvmptssdm  5721  unpreima  5762  respreima  5765  elrnrexdm  5776  elrnrexdmb  5777  rexrnmpt  5780  dffo4  5785  rnmptss  5798  funiun  5818  funopdmsn  5823  fvpr1  5847  fvpr2  5848  elunirn  5896  f1veqaeq  5899  isores1  5944  iotaexel  5965  riotauni  5967  riotacl2  5975  riota1  5980  riota1a  5981  snriota  5992  eusvobj2  5993  acexmidlema  5998  acexmidlemb  5999  acexmidlem2  6004  oprabid  6039  0neqopab  6055  brabvv  6056  1stval2  6307  2ndval2  6308  xp1st  6317  xp2nd  6318  unielxp  6326  releldm2  6337  cnvf1o  6377  fo2ndf  6379  poxp  6384  reldmtpos  6405  dftpos4  6415  tpostpos  6416  tpostpos2  6417  iunon  6436  smoel  6452  tfrlem4  6465  tfrlem7  6469  tfrlem8  6470  tfrlem9  6471  nnaord  6663  ecexr  6693  swoord1  6717  swoord2  6718  0er  6722  mapprc  6807  mapsnconst  6849  ixpf  6875  mptelixpg  6889  idssen  6936  ener  6939  en0  6955  en1  6959  en1bg  6960  2dom  6966  enm  6987  xpsnen  6988  ssenen  7020  snnen2og  7028  php5dom  7032  phpm  7035  findcard  7058  findcard2  7059  findcard2s  7060  unfiexmid  7091  fiintim  7104  fidcenumlemim  7130  sbthlem1  7135  fiss  7155  djuexb  7222  djuss  7248  eldju2ndl  7250  eldju2ndr  7251  ctssdclemr  7290  exmidlpo  7321  finnum  7366  ficardon  7372  exmidfodomrlemim  7390  acnrcl  7394  3nsssucpw1  7432  indpi  7540  subhalfnqq  7612  archnqq  7615  enq0sym  7630  nqnq0pi  7636  nqnq0  7639  mulnnnq0  7648  prml  7675  prmu  7676  prssnql  7677  prssnqu  7678  prcdnql  7682  prcunqu  7683  prltlu  7685  prnmaxl  7686  prnminu  7687  prloc  7689  prdisj  7690  addcanprg  7814  recexprlemopl  7823  recexprlemopu  7825  cauappcvgprlemladdfu  7852  caucvgprlemladdfu  7875  recexgt0sr  7971  renfdisj  8217  axsuploc  8230  negf1o  8539  recexre  8736  apsqgt0  8759  apreim  8761  aprcl  8804  recexaplem2  8810  rerecclap  8888  nn0ge0  9405  elnnnn0b  9424  xnn0xr  9448  xnn0nemnf  9454  xnn0nnn0pnf  9456  znegcl  9488  zeo  9563  nn0ind  9572  nn0ind-raph  9575  uzn0  9750  eluzaddi  9761  eluzsubi  9762  uznn0sub  9766  uz3m2nn  9780  uznnssnn  9784  uz2m1nn  9812  uz2mulcl  9815  indstr2  9816  qmulz  9830  qre  9832  qnegcl  9843  qreccl  9849  rphalflt  9891  nn0ledivnn  9975  xrltnr  9987  nltpnft  10022  ngtmnft  10025  xrrebnd  10027  xnegcl  10040  xnegneg  10041  xltnegi  10043  xrpnfdc  10050  xrmnfdc  10051  xnegid  10067  xaddid1  10070  xnn0lenn0nn0  10073  xnn0xadd0  10075  xposdif  10090  elioore  10120  elfzuz2  10237  uzsubsubfz  10255  fzdisj  10260  fzmmmeqm  10266  elfz0ubfz0  10333  elfz0fzfz0  10334  fz0fzelfz0  10335  fz0fzdiffz0  10338  elfzmlbp  10340  difelfzle  10342  difelfznle  10343  nn0disj  10346  2ffzeq  10349  fzo1fzo0n0  10395  elfzo0z  10396  elfzo0le  10397  fzonmapblen  10399  fzofzim  10400  elfzodifsumelfzo  10419  elfzonlteqm1  10428  fzonn0p1p1  10431  elfzom1p1elfzo  10432  ssfzo12bi  10443  ubmelm1fzo  10444  fzind2  10457  subfzo0  10460  infssuzcldc  10467  rebtwn2z  10486  fldiv4p1lem1div2  10537  fldiv4lem1div2  10539  flqeqceilz  10552  zmodidfzoimp  10588  modfzo0difsn  10629  nnsinds  10679  nn0sinds  10680  expcl2lemap  10785  qexpclz  10794  zzlesq  10942  facp1  10964  facnn2  10968  faclbnd3  10977  bcn1  10992  hashfz0  11060  wrdf  11090  swrdswrdlem  11251  swrdswrd  11252  swrdccatin1  11272  pfxccatin12lem2a  11274  pfxccatin12lem1  11275  swrdccatin2  11276  pfxccatin12lem2  11278  pfxccatin12lem3  11279  pfxccatin12  11280  pfxccat3  11281  swrdccat  11282  swrdccat3blem  11286  cvg1nlemres  11511  rexanuz  11514  fclim  11820  climmo  11824  iser3shft  11872  fsumsplitsn  11936  fsum2dlemstep  11960  fisumcom2  11964  arisum  12024  arisum2  12025  prodmodc  12104  fprodfac  12141  fprod2dlemstep  12148  fprodcom2fi  12152  fprodsplitsn  12159  eftlub  12216  ef01bndlem  12282  sin01gt0  12288  cos01gt0  12289  sin02gt0  12290  dvdsdivcl  12376  addmodlteqALT  12385  odd2np1  12399  oddge22np1  12407  m1expe  12425  nn0enne  12428  nn0o1gt2  12431  nno  12432  ndvdsadd  12457  dfgcd2  12550  mulgcd  12552  algfx  12589  prmind2  12657  prm2orodd  12663  prmgt1  12669  oddprmgt2  12671  dfphi2  12757  nnnn0modprm0  12793  prm23lt5  12801  pythagtriplem2  12804  pcz  12870  dvdsprmpweqnn  12874  oddprmdvds  12892  prmunb  12900  4sqlem4  12930  4sqlem19  12947  evenennn  12979  fngsum  13436  igsumvalx  13437  dfgrp3me  13648  mulgnn0gsum  13680  rngdi  13918  rngdir  13919  dvdsrcl2  14078  unitinvcl  14102  unitinvinv  14103  unitlinv  14105  unitrinv  14106  rmodislmodlem  14329  rmodislmod  14330  zrhval  14596  psrbagf  14649  distop  14774  ntrss  14808  ssntr  14811  lmrcl  14881  txuni2  14945  txcn  14964  hmeocnvb  15007  xmetunirn  15047  blssioo  15242  divcnap  15254  cdivcncfap  15293  dedekindeulemlub  15309  dedekindicclemlub  15318  dvexp2  15401  elply2  15424  plyco  15448  pilem3  15472  sincosq1sgn  15515  sincosq2sgn  15516  sincosq3sgn  15517  sincosq4sgn  15518  sinq12gt0  15519  fsumdvdsmul  15680  zabsle1  15693  lgsdir2lem4  15725  gausslemma2dlem0f  15748  gausslemma2dlem1a  15752  gausslemma2dlem2  15756  gausslemma2dlem3  15757  gausslemma2dlem4  15758  2lgslem1a1  15780  2lgslem3  15795  2lgsoddprmlem3  15805  2lgsoddprm  15807  2sqlem2  15809  2sqlem10  15819  vtxvalprc  15871  iedgvalprc  15872  upgrex  15918  umgredg  15958  ausgrusgrben  15981  usgruspgrben  15999  usgrislfuspgrdom  16003  uhgr2edg  16019  uspgredg2v  16034  wlkv  16067  wlk1walkdom  16100  trlsv  16123  trlf1  16126  clwwlk1loop  16136  bj-pm2.18st  16169  bj-dcstab  16175  decidi  16214  sumdc2  16218  bj-charfunbi  16229  bdel  16263  bdssex  16320  bj-indind  16350  findset  16363  nninfall  16435  trirec0  16472  neap0mkv  16497