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  dcor  936  pm5.62dc  946  pm5.63dc  947  pm4.83dc  952  3simpb  996  3simpc  997  3imp  1194  3com12  1208  3com13  1209  syl3anb  1291  xoranor  1387  xorbin  1394  xordc1  1403  biassdc  1405  nfr  1528  nfand  1578  19.21t  1592  19.30dc  1637  exintrbi  1643  19.9t  1652  nfnt  1666  equveli  1769  exdistrfor  1810  sbcof2  1820  sbidm  1861  sbi1v  1901  sbalyz  2009  sbal1yz  2011  nfsb4t  2024  euex  2066  eumo0  2067  mor  2078  exmodc  2086  mo3h  2089  mopick  2114  moexexdc  2120  euexex  2121  2euex  2123  exists2  2133  eqcoms  2190  eleq2s  2282  nfcr  2321  necon3ai  2406  rexnalim  2476  dfrex2dc  2478  rexex  2533  rsp  2534  ralim  2546  rexim  2581  r19.32r  2633  r19.44av  2646  r19.45av  2647  gencl  2781  gencbvex  2795  gencbval  2797  vtoclgf  2807  vtoclg1f  2808  pm13.183  2887  elrabi  2902  eueq2dc  2922  eueq3dc  2923  mob2  2929  euxfr2dc  2934  reu3  2939  rmoim  2950  2rmorex  2955  sbcex  2983  sbcbi2  3025  ra5  3063  sseq1  3190  difdif  3272  dfss4st  3380  difindiss  3401  undif3ss  3408  dfrab3ss  3425  abvor0dc  3458  reldisj  3486  disjel  3489  inssdif0im  3502  uneqdifeqim  3520  r19.2m  3521  r19.2mOLD  3522  r19.3rm  3523  r19.9rmv  3526  rexm  3534  ralm  3539  raaanlem  3540  ifnefalse  3557  ifnotdc  3583  ifandc  3584  ifmdc  3586  nelpri  3628  nelprd  3630  prprc1  3712  difprsn2  3744  diftpsn3  3745  snsssn  3773  preqr2  3781  preq12b  3782  opthpr  3784  prneimg  3786  oprcl  3814  pwprss  3817  intmin4  3884  uniintabim  3893  dfiin2g  3931  iinss2  3951  iundif2ss  3964  disjnim  4006  disjnims  4007  invdisj  4009  disjiun  4010  brne0  4064  brm  4065  trel  4120  trss  4122  ssex  4152  bnd2  4185  abssexg  4194  exmidexmid  4208  rext  4227  unipw  4229  euabex  4237  mss  4238  exss  4239  copsexg  4256  opelopabsb  4272  pwssunim  4296  epelg  4302  sowlin  4332  sotritric  4336  elsuci  4415  sucprc  4424  reusv3  4472  ordon  4497  onsucmin  4518  onsucelsucr  4519  unon  4522  onsucelsucexmid  4541  setind  4550  setind2  4551  sucprcreg  4560  en2lp  4565  eunex  4572  ordsoexmid  4573  ordpwsucss  4578  tfi  4593  peano1  4605  peano2  4606  find  4610  0nelelxp  4667  opelxp  4668  elvvuni  4702  optocl  4714  ralxpf  4785  rexxpf  4786  relop  4789  breldm  4843  dmxpm  4859  elreldm  4865  dmrnssfld  4902  dmcosseq  4910  resabs1  4948  resima2  4953  issref  5023  asymref  5026  xpidtr  5031  trin2  5032  poirr2  5033  xpmlem  5061  dmxpss  5071  xp11m  5079  cnveqb  5096  dfco2a  5141  cores2  5153  coi2  5157  relcnvtr  5160  relresfld  5170  relcnvexb  5180  cnviinm  5182  iotauni  5202  iota1  5204  iota4  5208  iotam  5220  dffun8  5256  funcnvsn  5273  imadif  5308  imainlem  5309  fcoi1  5408  fcoi2  5409  f0rn0  5422  f1ocnv  5486  f1ocnvb  5487  fun11iun  5494  ffoss  5505  f1o00  5508  fo00  5509  relelfvdm  5559  nfvres  5560  nfunsn  5561  ssimaex  5590  fvmptss2  5604  fvmptssdm  5613  unpreima  5654  respreima  5657  elrnrexdm  5668  elrnrexdmb  5669  rexrnmpt  5672  dffo4  5677  rnmptss  5690  fvpr1  5733  fvpr2  5734  elunirn  5780  f1veqaeq  5783  isores1  5828  riotauni  5850  riotacl2  5857  riota1  5862  riota1a  5863  snriota  5873  eusvobj2  5874  acexmidlema  5879  acexmidlemb  5880  acexmidlem2  5885  oprabid  5920  0neqopab  5933  brabvv  5934  1stval2  6169  2ndval2  6170  xp1st  6179  xp2nd  6180  unielxp  6188  releldm2  6199  cnvf1o  6239  fo2ndf  6241  poxp  6246  reldmtpos  6267  dftpos4  6277  tpostpos  6278  tpostpos2  6279  iunon  6298  smoel  6314  tfrlem4  6327  tfrlem7  6331  tfrlem8  6332  tfrlem9  6333  nnaord  6523  ecexr  6553  swoord1  6577  swoord2  6578  0er  6582  mapprc  6665  mapsnconst  6707  ixpf  6733  mptelixpg  6747  idssen  6790  ener  6792  en0  6808  en1  6812  en1bg  6813  2dom  6818  enm  6833  xpsnen  6834  ssenen  6864  snnen2og  6872  php5dom  6876  phpm  6878  findcard  6901  findcard2  6902  findcard2s  6903  unfiexmid  6930  fiintim  6941  fidcenumlemim  6964  sbthlem1  6969  fiss  6989  djuexb  7056  djuss  7082  eldju2ndl  7084  eldju2ndr  7085  ctssdclemr  7124  exmidlpo  7154  finnum  7195  exmidfodomrlemim  7213  3nsssucpw1  7248  indpi  7354  subhalfnqq  7426  archnqq  7429  enq0sym  7444  nqnq0pi  7450  nqnq0  7453  mulnnnq0  7462  prml  7489  prmu  7490  prssnql  7491  prssnqu  7492  prcdnql  7496  prcunqu  7497  prltlu  7499  prnmaxl  7500  prnminu  7501  prloc  7503  prdisj  7504  addcanprg  7628  recexprlemopl  7637  recexprlemopu  7639  cauappcvgprlemladdfu  7666  caucvgprlemladdfu  7689  recexgt0sr  7785  renfdisj  8030  axsuploc  8043  negf1o  8352  recexre  8548  apsqgt0  8571  apreim  8573  aprcl  8616  recexaplem2  8622  rerecclap  8700  nn0ge0  9214  elnnnn0b  9233  xnn0xr  9257  xnn0nemnf  9263  xnn0nnn0pnf  9265  znegcl  9297  zeo  9371  nn0ind  9380  nn0ind-raph  9383  uzn0  9556  eluzaddi  9567  eluzsubi  9568  uznn0sub  9572  uz3m2nn  9586  uznnssnn  9590  uz2m1nn  9618  uz2mulcl  9621  indstr2  9622  qmulz  9636  qre  9638  qnegcl  9649  qreccl  9655  rphalflt  9696  nn0ledivnn  9780  xrltnr  9792  nltpnft  9827  ngtmnft  9830  xrrebnd  9832  xnegcl  9845  xnegneg  9846  xltnegi  9848  xrpnfdc  9855  xrmnfdc  9856  xnegid  9872  xaddid1  9875  xnn0lenn0nn0  9878  xnn0xadd0  9880  xposdif  9895  elioore  9925  elfzuz2  10042  uzsubsubfz  10060  fzdisj  10065  fzmmmeqm  10071  elfz0ubfz0  10138  elfz0fzfz0  10139  fz0fzelfz0  10140  fz0fzdiffz0  10143  elfzmlbp  10145  difelfzle  10147  difelfznle  10148  nn0disj  10151  2ffzeq  10154  fzo1fzo0n0  10196  elfzo0z  10197  elfzo0le  10198  fzonmapblen  10200  fzofzim  10201  elfzodifsumelfzo  10214  elfzonlteqm1  10223  fzonn0p1p1  10226  elfzom1p1elfzo  10227  ssfzo12bi  10238  ubmelm1fzo  10239  fzind2  10252  subfzo0  10255  rebtwn2z  10268  fldiv4p1lem1div2  10318  flqeqceilz  10331  zmodidfzoimp  10367  modfzo0difsn  10408  nnsinds  10456  nn0sinds  10457  expcl2lemap  10545  qexpclz  10554  facp1  10723  facnn2  10727  faclbnd3  10736  bcn1  10751  hashfz0  10818  cvg1nlemres  11007  rexanuz  11010  fclim  11315  climmo  11319  iser3shft  11367  fsumsplitsn  11431  fsum2dlemstep  11455  fisumcom2  11459  arisum  11519  arisum2  11520  prodmodc  11599  fprodfac  11636  fprod2dlemstep  11643  fprodcom2fi  11647  fprodsplitsn  11654  eftlub  11711  ef01bndlem  11777  sin01gt0  11782  cos01gt0  11783  sin02gt0  11784  dvdsdivcl  11869  addmodlteqALT  11878  odd2np1  11891  oddge22np1  11899  m1expe  11917  nn0enne  11920  nn0o1gt2  11923  nno  11924  ndvdsadd  11949  infssuzcldc  11965  dfgcd2  12028  mulgcd  12030  algfx  12065  prmind2  12133  prm2orodd  12139  prmgt1  12145  oddprmgt2  12147  dfphi2  12233  nnnn0modprm0  12268  prm23lt5  12276  pythagtriplem2  12279  pcz  12344  dvdsprmpweqnn  12348  oddprmdvds  12365  prmunb  12373  4sqlem4  12403  evenennn  12407  dfgrp3me  12996  rngdi  13190  rngdir  13191  dvdsrcl2  13342  unitinvcl  13366  unitinvinv  13367  unitlinv  13369  unitrinv  13370  rmodislmodlem  13534  rmodislmod  13535  distop  13856  ntrss  13890  ssntr  13893  lmrcl  13962  lmreltop  13964  txuni2  14027  txcn  14046  hmeocnvb  14089  xmetunirn  14129  blssioo  14316  divcnap  14326  cdivcncfap  14358  dedekindeulemlub  14369  dedekindicclemlub  14378  dvexp2  14447  pilem3  14475  sincosq1sgn  14518  sincosq2sgn  14519  sincosq3sgn  14520  sincosq4sgn  14521  sinq12gt0  14522  zabsle1  14671  lgsdir2lem4  14703  2lgsoddprmlem3  14730  2sqlem2  14733  2sqlem10  14743  bj-pm2.18st  14773  bj-dcstab  14779  decidi  14818  sumdc2  14822  bj-charfunbi  14834  bdel  14868  bdssex  14925  bj-indind  14955  findset  14968  nninfall  15030  trirec0  15064  neap0mkv  15089