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  588  sylnbi  679  dcim  842  notnotrdc  844  condcOLD  855  pm2.61ddc  862  pm5.18dc  884  pm2.25dc  894  pm2.85dc  906  pm5.12dc  911  pm5.14dc  912  pm5.55dc  914  peircedc  915  pm5.54dc  919  dcand  934  dcor  937  pm5.62dc  947  pm5.63dc  948  pm4.83dc  953  3simpb  997  3simpc  998  3imp  1195  3com12  1209  3com13  1210  syl3anb  1292  xoranor  1388  xorbin  1395  xordc1  1404  biassdc  1406  nfr  1532  nfand  1582  19.21t  1596  19.30dc  1641  exintrbi  1647  19.9t  1656  nfnt  1670  equveli  1773  exdistrfor  1814  sbcof2  1824  sbidm  1865  sbi1v  1906  sbalyz  2018  sbal1yz  2020  nfsb4t  2033  euex  2075  eumo0  2076  mor  2087  exmodc  2095  mo3h  2098  mopick  2123  moexexdc  2129  euexex  2130  2euex  2132  exists2  2142  eqcoms  2199  eleq2s  2291  nfcr  2331  necon3ai  2416  rexnalim  2486  dfrex2dc  2488  rexex  2543  rsp  2544  ralim  2556  rexim  2591  r19.32r  2643  r19.44av  2656  r19.45av  2657  gencl  2795  gencbvex  2810  gencbval  2812  vtoclgf  2822  vtoclg1f  2823  pm13.183  2902  elrabi  2917  eueq2dc  2937  eueq3dc  2938  mob2  2944  euxfr2dc  2949  reu3  2954  rmoim  2965  2rmorex  2970  sbcex  2998  sbcbi2  3040  ra5  3078  sseq1  3207  difdif  3289  dfss4st  3397  difindiss  3418  undif3ss  3425  dfrab3ss  3442  abvor0dc  3475  reldisj  3503  disjel  3506  inssdif0im  3519  uneqdifeqim  3537  r19.2m  3538  r19.2mOLD  3539  r19.3rm  3540  r19.9rmv  3543  rexm  3551  ralm  3555  raaanlem  3556  ifnefalse  3573  ifnotdc  3599  ifandc  3600  ifmdc  3602  nelpri  3647  nelprd  3649  prprc1  3731  difprsn2  3763  diftpsn3  3764  snsssn  3792  preqr2  3800  preq12b  3801  opthpr  3803  prneimg  3805  oprcl  3833  pwprss  3836  intmin4  3903  uniintabim  3912  dfiin2g  3950  iinss2  3970  iundif2ss  3983  disjnim  4025  disjnims  4026  invdisj  4028  disjiun  4029  brne0  4083  brm  4084  trel  4139  trss  4141  ssex  4171  bnd2  4207  abssexg  4216  exmidexmid  4230  rext  4249  unipw  4251  euabex  4259  mss  4260  exss  4261  copsexg  4278  opelopabsb  4295  pwssunim  4320  epelg  4326  sowlin  4356  sotritric  4360  elsuci  4439  sucprc  4448  reusv3  4496  ordon  4523  onsucmin  4544  onsucelsucr  4545  unon  4548  onsucelsucexmid  4567  setind  4576  setind2  4577  sucprcreg  4586  en2lp  4591  eunex  4598  ordsoexmid  4599  ordpwsucss  4604  tfi  4619  peano1  4631  peano2  4632  find  4636  0nelelxp  4693  opelxp  4694  elvvuni  4728  optocl  4740  ralxpf  4813  rexxpf  4814  relop  4817  breldm  4871  dmxpm  4887  elreldm  4893  dmrnssfld  4930  dmcosseq  4938  resabs1  4976  resima2  4981  issref  5053  asymref  5056  xpidtr  5061  trin2  5062  poirr2  5063  xpmlem  5091  dmxpss  5101  xp11m  5109  cnveqb  5126  dfco2a  5171  cores2  5183  coi2  5187  relcnvtr  5190  relresfld  5200  relcnvexb  5210  cnviinm  5212  iotauni  5232  iota1  5234  iota4  5239  iotam  5251  dffun8  5287  funcnvsn  5304  imadif  5339  imainlem  5340  fcoi1  5441  fcoi2  5442  f0rn0  5455  f1ocnv  5520  f1ocnvb  5521  fun11iun  5528  ffoss  5539  f1o00  5542  fo00  5543  relelfvdm  5593  nfvres  5595  nfunsn  5596  ssimaex  5625  fvmptss2  5639  fvmptssdm  5649  unpreima  5690  respreima  5693  elrnrexdm  5704  elrnrexdmb  5705  rexrnmpt  5708  dffo4  5713  rnmptss  5726  fvpr1  5769  fvpr2  5770  elunirn  5816  f1veqaeq  5819  isores1  5864  iotaexel  5885  riotauni  5887  riotacl2  5894  riota1  5899  riota1a  5900  snriota  5910  eusvobj2  5911  acexmidlema  5916  acexmidlemb  5917  acexmidlem2  5922  oprabid  5957  0neqopab  5971  brabvv  5972  1stval2  6222  2ndval2  6223  xp1st  6232  xp2nd  6233  unielxp  6241  releldm2  6252  cnvf1o  6292  fo2ndf  6294  poxp  6299  reldmtpos  6320  dftpos4  6330  tpostpos  6331  tpostpos2  6332  iunon  6351  smoel  6367  tfrlem4  6380  tfrlem7  6384  tfrlem8  6385  tfrlem9  6386  nnaord  6576  ecexr  6606  swoord1  6630  swoord2  6631  0er  6635  mapprc  6720  mapsnconst  6762  ixpf  6788  mptelixpg  6802  idssen  6845  ener  6847  en0  6863  en1  6867  en1bg  6868  2dom  6873  enm  6888  xpsnen  6889  ssenen  6921  snnen2og  6929  php5dom  6933  phpm  6935  findcard  6958  findcard2  6959  findcard2s  6960  unfiexmid  6988  fiintim  7001  fidcenumlemim  7027  sbthlem1  7032  fiss  7052  djuexb  7119  djuss  7145  eldju2ndl  7147  eldju2ndr  7148  ctssdclemr  7187  exmidlpo  7218  finnum  7261  ficardon  7267  exmidfodomrlemim  7280  acnrcl  7284  3nsssucpw1  7319  indpi  7426  subhalfnqq  7498  archnqq  7501  enq0sym  7516  nqnq0pi  7522  nqnq0  7525  mulnnnq0  7534  prml  7561  prmu  7562  prssnql  7563  prssnqu  7564  prcdnql  7568  prcunqu  7569  prltlu  7571  prnmaxl  7572  prnminu  7573  prloc  7575  prdisj  7576  addcanprg  7700  recexprlemopl  7709  recexprlemopu  7711  cauappcvgprlemladdfu  7738  caucvgprlemladdfu  7761  recexgt0sr  7857  renfdisj  8103  axsuploc  8116  negf1o  8425  recexre  8622  apsqgt0  8645  apreim  8647  aprcl  8690  recexaplem2  8696  rerecclap  8774  nn0ge0  9291  elnnnn0b  9310  xnn0xr  9334  xnn0nemnf  9340  xnn0nnn0pnf  9342  znegcl  9374  zeo  9448  nn0ind  9457  nn0ind-raph  9460  uzn0  9634  eluzaddi  9645  eluzsubi  9646  uznn0sub  9650  uz3m2nn  9664  uznnssnn  9668  uz2m1nn  9696  uz2mulcl  9699  indstr2  9700  qmulz  9714  qre  9716  qnegcl  9727  qreccl  9733  rphalflt  9775  nn0ledivnn  9859  xrltnr  9871  nltpnft  9906  ngtmnft  9909  xrrebnd  9911  xnegcl  9924  xnegneg  9925  xltnegi  9927  xrpnfdc  9934  xrmnfdc  9935  xnegid  9951  xaddid1  9954  xnn0lenn0nn0  9957  xnn0xadd0  9959  xposdif  9974  elioore  10004  elfzuz2  10121  uzsubsubfz  10139  fzdisj  10144  fzmmmeqm  10150  elfz0ubfz0  10217  elfz0fzfz0  10218  fz0fzelfz0  10219  fz0fzdiffz0  10222  elfzmlbp  10224  difelfzle  10226  difelfznle  10227  nn0disj  10230  2ffzeq  10233  fzo1fzo0n0  10276  elfzo0z  10277  elfzo0le  10278  fzonmapblen  10280  fzofzim  10281  elfzodifsumelfzo  10294  elfzonlteqm1  10303  fzonn0p1p1  10306  elfzom1p1elfzo  10307  ssfzo12bi  10318  ubmelm1fzo  10319  fzind2  10332  subfzo0  10335  infssuzcldc  10342  rebtwn2z  10361  fldiv4p1lem1div2  10412  fldiv4lem1div2  10414  flqeqceilz  10427  zmodidfzoimp  10463  modfzo0difsn  10504  nnsinds  10554  nn0sinds  10555  expcl2lemap  10660  qexpclz  10669  zzlesq  10817  facp1  10839  facnn2  10843  faclbnd3  10852  bcn1  10867  hashfz0  10934  wrdf  10958  cvg1nlemres  11167  rexanuz  11170  fclim  11476  climmo  11480  iser3shft  11528  fsumsplitsn  11592  fsum2dlemstep  11616  fisumcom2  11620  arisum  11680  arisum2  11681  prodmodc  11760  fprodfac  11797  fprod2dlemstep  11804  fprodcom2fi  11808  fprodsplitsn  11815  eftlub  11872  ef01bndlem  11938  sin01gt0  11944  cos01gt0  11945  sin02gt0  11946  dvdsdivcl  12032  addmodlteqALT  12041  odd2np1  12055  oddge22np1  12063  m1expe  12081  nn0enne  12084  nn0o1gt2  12087  nno  12088  ndvdsadd  12113  dfgcd2  12206  mulgcd  12208  algfx  12245  prmind2  12313  prm2orodd  12319  prmgt1  12325  oddprmgt2  12327  dfphi2  12413  nnnn0modprm0  12449  prm23lt5  12457  pythagtriplem2  12460  pcz  12526  dvdsprmpweqnn  12530  oddprmdvds  12548  prmunb  12556  4sqlem4  12586  4sqlem19  12603  evenennn  12635  fngsum  13090  igsumvalx  13091  dfgrp3me  13302  mulgnn0gsum  13334  rngdi  13572  rngdir  13573  dvdsrcl2  13731  unitinvcl  13755  unitinvinv  13756  unitlinv  13758  unitrinv  13759  rmodislmodlem  13982  rmodislmod  13983  zrhval  14249  psrbagf  14300  distop  14405  ntrss  14439  ssntr  14442  lmrcl  14511  lmreltop  14513  txuni2  14576  txcn  14595  hmeocnvb  14638  xmetunirn  14678  blssioo  14873  divcnap  14885  cdivcncfap  14924  dedekindeulemlub  14940  dedekindicclemlub  14949  dvexp2  15032  elply2  15055  plyco  15079  pilem3  15103  sincosq1sgn  15146  sincosq2sgn  15147  sincosq3sgn  15148  sincosq4sgn  15149  sinq12gt0  15150  fsumdvdsmul  15311  zabsle1  15324  lgsdir2lem4  15356  gausslemma2dlem0f  15379  gausslemma2dlem1a  15383  gausslemma2dlem2  15387  gausslemma2dlem3  15388  gausslemma2dlem4  15389  2lgslem1a1  15411  2lgslem3  15426  2lgsoddprmlem3  15436  2lgsoddprm  15438  2sqlem2  15440  2sqlem10  15450  bj-pm2.18st  15480  bj-dcstab  15486  decidi  15525  sumdc2  15529  bj-charfunbi  15541  bdel  15575  bdssex  15632  bj-indind  15662  findset  15675  nninfall  15740  trirec0  15775  neap0mkv  15800