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  685  dcim  849  notnotrdc  851  condcOLD  862  pm2.61ddc  869  pm5.18dc  891  pm2.25dc  901  pm2.85dc  913  pm5.12dc  918  pm5.14dc  919  pm5.55dc  921  peircedc  922  pm5.54dc  926  dcand  941  dcor  944  pm5.62dc  954  pm5.63dc  955  pm4.83dc  960  ifp2  989  ifpor  996  1fpid3  1003  3simpb  1022  3simpc  1023  3imp  1220  3com12  1234  3com13  1235  syl3anb  1317  xoranor  1422  xorbin  1429  xordc1  1438  biassdc  1440  nfr  1567  nfand  1617  19.21t  1631  19.30dc  1676  exintrbi  1682  19.9t  1691  nfnt  1704  equveli  1808  exdistrfor  1849  sbcof2  1859  sbidm  1900  sbi1v  1942  sbalyz  2055  sbal1yz  2057  nfsb4t  2070  euex  2112  eumo0  2113  mor  2125  exmodc  2133  mo3h  2136  mopick  2161  moexexdc  2167  euexex  2168  2euex  2170  exists2  2180  eqcoms  2237  eleq2s  2329  nfcr  2378  necon3ai  2463  rexnalim  2533  dfrex2dc  2535  rexex  2590  rsp  2591  ralim  2603  rexim  2638  r19.32r  2691  r19.44av  2704  r19.45av  2705  gencl  2848  gencbvex  2863  gencbval  2865  vtoclgf  2875  vtoclg1f  2876  pm13.183  2958  elrabi  2973  eueq2dc  2993  eueq3dc  2994  mob2  3000  euxfr2dc  3005  reu3  3010  rmoim  3021  2rmorex  3026  sbcex  3054  sbcbi2  3096  ra5  3135  sseq1  3265  difdif  3348  dfss4st  3458  difindiss  3479  undif3ss  3486  dfrab3ss  3503  abvor0dc  3536  reldisj  3564  disjel  3567  inssdif0im  3580  uneqdifeqim  3599  r19.2m  3600  r19.2mOLD  3601  r19.3rm  3602  r19.9rmv  3605  rexm  3613  ralm  3617  raaanlem  3618  ifnefalse  3637  ifnotdc  3665  ifandc  3667  ifmdc  3669  nelpri  3718  nelprd  3720  prprc1  3805  difprsn2  3839  diftpsn3  3840  snsssn  3870  preqr2  3878  preq12b  3879  opthpr  3881  prneimg  3883  oprcl  3912  pwprss  3915  intmin4  3982  uniintabim  3991  dfiin2g  4029  iinss2  4049  iundif2ss  4062  disjnim  4104  disjnims  4105  invdisj  4107  disjiun  4109  brne0  4164  brm  4165  trel  4220  trss  4222  ssex  4252  bnd2  4291  abssexg  4300  exmidexmid  4314  rext  4336  unipw  4338  euabex  4346  mss  4347  exss  4348  copsexg  4365  opelopabsb  4383  pwssunim  4410  epelg  4416  sowlin  4446  sotritric  4450  elsuci  4529  sucprc  4538  reusv3  4586  ordon  4613  onsucmin  4634  onsucelsucr  4635  unon  4638  onsucelsucexmid  4657  setind  4666  setind2  4667  sucprcreg  4676  en2lp  4681  eunex  4688  ordsoexmid  4689  ordpwsucss  4694  tfi  4709  peano1  4721  peano2  4722  find  4726  0nelelxp  4783  opelxp  4784  elvvuni  4819  optocl  4831  ralxpf  4906  rexxpf  4907  relop  4910  breldm  4965  reldmm  4980  dmxpm  4982  elreldm  4988  dmrnssfld  5025  dmcosseq  5034  resabs1  5072  resima2  5077  issref  5150  asymref  5153  xpidtr  5158  trin2  5159  poirr2  5160  xpmlem  5188  dmxpss  5198  xp11m  5206  cnveqb  5223  dfco2a  5268  cores2  5280  coi2  5284  relcnvtr  5287  relresfld  5297  relcnvexb  5307  cnviinm  5309  iotauni  5330  iota1  5332  iota4  5337  iotam  5349  dffun8  5385  fununfun  5404  funcnvsn  5406  imadif  5441  imainlem  5442  fcoi1  5552  fcoi2  5553  f0rn0  5567  f1ocnv  5632  f1ocnvb  5633  fun11iun  5640  ffoss  5652  f1o00  5656  fo00  5657  relelfvdm  5707  nfvres  5711  nfunsn  5712  ssimaex  5743  fvmptss2  5757  fvmptssdm  5767  unpreima  5807  respreima  5810  elrnrexdm  5821  elrnrexdmb  5822  rexrnmpt  5825  dffo4  5830  rnmptss  5843  funiun  5864  funopdmsn  5869  fvpr1  5893  fvpr2  5894  elunirn  5945  f1veqaeq  5948  isores1  5993  iotaexel  6016  riotauni  6018  riotacl2  6026  riota1  6031  riota1a  6032  snriota  6043  eusvobj2  6044  acexmidlema  6049  acexmidlemb  6050  acexmidlem2  6055  oprabid  6090  0neqopab  6106  brabvv  6107  1stval2  6362  2ndval2  6363  xp1st  6372  xp2nd  6373  unielxp  6381  releldm2  6392  cnvf1o  6434  fo2ndf  6436  poxp  6441  reldmtpos  6497  dftpos4  6507  tpostpos  6508  tpostpos2  6509  iunon  6528  smoel  6544  tfrlem4  6557  tfrlem7  6561  tfrlem8  6562  tfrlem9  6563  nnaord  6755  ecexr  6785  swoord1  6809  swoord2  6810  0er  6814  mapprc  6899  mapsnconst  6942  ixpf  6968  mptelixpg  6982  idssen  7029  ener  7032  en0  7048  en1  7052  en1bg  7053  2dom  7059  modom  7074  enm  7084  xpsnen  7085  ssenen  7118  snnen2og  7126  php5dom  7130  phpm  7133  findcard  7158  findcard2  7159  findcard2s  7160  unfiexmid  7191  fiintim  7204  fidcenumlemim  7235  sbthlem1  7240  fiss  7277  djuexb  7348  djuss  7374  eldju2ndl  7376  eldju2ndr  7377  ctssdclemr  7416  exmidlpo  7447  finnum  7492  ficardon  7498  exmidfodomrlemim  7517  acnrcl  7521  3nsssucpw1  7559  indpi  7673  subhalfnqq  7745  archnqq  7748  enq0sym  7763  nqnq0pi  7769  nqnq0  7772  mulnnnq0  7781  prml  7808  prmu  7809  prssnql  7810  prssnqu  7811  prcdnql  7815  prcunqu  7816  prltlu  7818  prnmaxl  7819  prnminu  7820  prloc  7822  prdisj  7823  addcanprg  7947  recexprlemopl  7956  recexprlemopu  7958  cauappcvgprlemladdfu  7985  caucvgprlemladdfu  8008  recexgt0sr  8104  renfdisj  8349  axsuploc  8362  negf1o  8672  recexre  8869  apsqgt0  8892  apreim  8894  aprcl  8937  recexaplem2  8943  rerecclap  9021  nn0ge0  9538  elnnnn0b  9557  xnn0xr  9585  xnn0nemnf  9591  xnn0nnn0pnf  9593  znegcl  9625  zeo  9701  nn0ind  9710  nn0ind-raph  9713  uzn0  9888  eluzaddi  9899  eluzsubi  9900  uznn0sub  9904  uz3m2nn  9923  uznnssnn  9927  uz2m1nn  9955  uz2mulcl  9958  indstr2  9959  qmulz  9973  qre  9975  qnegcl  9986  qreccl  9992  rphalflt  10034  nn0ledivnn  10118  xrltnr  10131  nltpnft  10166  ngtmnft  10169  xrrebnd  10171  xnegcl  10184  xnegneg  10185  xltnegi  10187  xrpnfdc  10194  xrmnfdc  10195  xnegid  10211  xaddid1  10214  xnn0lenn0nn0  10217  xnn0xadd0  10219  xposdif  10234  elioore  10264  elfzuz2  10383  uzsubsubfz  10401  fzdisj  10406  fzmmmeqm  10413  elfz0ubfz0  10481  elfz0fzfz0  10482  fz0fzelfz0  10483  fz0fzdiffz0  10486  elfzmlbp  10488  difelfzle  10490  difelfznle  10491  nn0disj  10494  2ffzeq  10497  fzo1fzo0n0  10544  elfzo0z  10545  elfzo0le  10546  fzonmapblen  10548  fzofzim  10549  elfzodifsumelfzo  10568  elfzonlteqm1  10577  fzonn0p1p1  10580  elfzom1p1elfzo  10581  ssfzo12bi  10592  ubmelm1fzo  10593  fzind2  10607  subfzo0  10610  infssuzcldc  10617  rebtwn2z  10638  fldiv4p1lem1div2  10689  fldiv4lem1div2  10691  flqeqceilz  10704  zmodidfzoimp  10740  modfzo0difsn  10781  nnsinds  10831  nn0sinds  10832  expcl2lemap  10937  qexpclz  10946  zzlesq  11095  facp1  11117  facnn2  11121  faclbnd3  11130  bcn1  11145  hashfz0  11215  hashfibc  11232  wrdf  11255  swrdswrdlem  11421  swrdswrd  11422  swrdccatin1  11442  pfxccatin12lem2a  11444  pfxccatin12lem1  11445  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12lem3  11449  pfxccatin12  11450  pfxccat3  11451  swrdccat  11452  swrdccat3blem  11456  cvg1nlemres  11695  rexanuz  11698  fclim  12004  climmo  12008  iser3shft  12056  fsumsplitsn  12121  fsum2dlemstep  12145  fisumcom2  12149  arisum  12209  arisum2  12210  prodmodc  12289  fprodfac  12326  fprod2dlemstep  12333  fprodcom2fi  12337  fprodsplitsn  12344  eftlub  12401  ef01bndlem  12467  sin01gt0  12473  cos01gt0  12474  sin02gt0  12475  dvdsdivcl  12561  addmodlteqALT  12570  odd2np1  12584  oddge22np1  12592  m1expe  12610  nn0enne  12613  nn0o1gt2  12616  nno  12617  ndvdsadd  12642  dfgcd2  12735  mulgcd  12737  algfx  12774  prmind2  12842  prm2orodd  12848  prmgt1  12854  oddprmgt2  12856  dfphi2  12942  nnnn0modprm0  12978  prm23lt5  12986  pythagtriplem2  12989  pcz  13055  dvdsprmpweqnn  13059  oddprmdvds  13077  prmunb  13085  4sqlem4  13115  4sqlem19  13132  ballotfilem2  13172  ballotfilem7  13223  evenennn  13228  fngsum  13651  igsumvalx  13652  dfgrp3me  13855  mulgnn0gsum  13881  rngdi  14179  rngdir  14180  dvdsrcl2  14344  unitinvcl  14368  unitinvinv  14369  unitlinv  14371  unitrinv  14372  opprdrng  14558  rmodislmodlem  14624  rmodislmod  14625  zrhval  14891  psrbagf  14944  distop  15076  ntrss  15110  ssntr  15113  lmrcl  15183  txuni2  15247  txcn  15266  hmeocnvb  15309  xmetunirn  15349  blssioo  15544  divcnap  15556  cdivcncfap  15595  dedekindeulemlub  15611  dedekindicclemlub  15620  dvexp2  15703  elply2  15726  plyco  15750  pilem3  15774  sincosq1sgn  15817  sincosq2sgn  15818  sincosq3sgn  15819  sincosq4sgn  15820  sinq12gt0  15821  fsumdvdsmul  15985  zabsle1  15998  lgsdir2lem4  16030  gausslemma2dlem0f  16053  gausslemma2dlem1a  16057  gausslemma2dlem2  16061  gausslemma2dlem3  16062  gausslemma2dlem4  16063  2lgslem1a1  16085  2lgslem3  16100  2lgsoddprmlem3  16110  2lgsoddprm  16112  2sqlem2  16114  2sqlem10  16124  vtxvalprc  16176  iedgvalprc  16177  upgrex  16224  umgredg  16266  ausgrusgrben  16289  usgruspgrben  16307  usgrislfuspgrdom  16311  uhgr2edg  16327  uspgredg2v  16342  griedg0ssusgr  16372  subusgr  16396  wlkv  16447  wlk1walkdom  16480  trlsv  16505  trlf1  16509  clwwlk1loop  16520  clwwlkext2edg  16543  umgr2cwwkdifex  16546  clwwlknonex2lem2  16559  clwwlknonex2e  16561  eupthv  16567  eupth2lem3lem4fi  16594  konigsberglem5  16613  bj-pm2.18st  16648  bj-dcstab  16654  decidi  16693  sumdc2  16697  bj-charfunbi  16707  bdel  16741  bdssex  16798  bj-indind  16828  findset  16841  nninfall  16913  trirec0  16954  neap0mkv  16981