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  3565  disjel  3568  inssdif0im  3581  uneqdifeqim  3600  r19.2m  3601  r19.2mOLD  3602  r19.3rm  3603  r19.9rmv  3606  rexm  3614  ralm  3618  raaanlem  3619  ifnefalse  3638  ifnotdc  3666  ifandc  3668  ifmdc  3670  nelpri  3719  nelprd  3721  prprc1  3806  difprsn2  3840  diftpsn3  3841  snsssn  3871  preqr2  3879  preq12b  3880  opthpr  3882  prneimg  3884  oprcl  3913  pwprss  3916  intmin4  3983  uniintabim  3992  dfiin2g  4030  iinss2  4050  iundif2ss  4063  disjnim  4105  disjnims  4106  invdisj  4108  disjiun  4110  brne0  4165  brm  4166  trel  4221  trss  4223  ssex  4253  bnd2  4292  abssexg  4301  exmidexmid  4315  rext  4337  unipw  4339  euabex  4347  mss  4348  exss  4349  copsexg  4366  opelopabsb  4384  pwssunim  4411  epelg  4417  sowlin  4447  sotritric  4451  elsuci  4530  sucprc  4539  reusv3  4587  ordon  4614  onsucmin  4635  onsucelsucr  4636  unon  4639  onsucelsucexmid  4658  setind  4667  setind2  4668  sucprcreg  4677  en2lp  4682  eunex  4689  ordsoexmid  4690  ordpwsucss  4695  tfi  4710  peano1  4722  peano2  4723  find  4727  0nelelxp  4784  opelxp  4785  elvvuni  4820  optocl  4832  ralxpf  4907  rexxpf  4908  relop  4911  breldm  4966  reldmm  4981  dmxpm  4983  elreldm  4989  dmrnssfld  5026  dmcosseq  5035  resabs1  5073  resima2  5078  issref  5151  asymref  5154  xpidtr  5159  trin2  5160  poirr2  5161  xpmlem  5189  dmxpss  5199  xp11m  5207  cnveqb  5224  dfco2a  5269  cores2  5281  coi2  5285  relcnvtr  5288  relresfld  5298  relcnvexb  5308  cnviinm  5310  iotauni  5331  iota1  5333  iota4  5338  iotam  5350  dffun8  5386  fununfun  5405  funcnvsn  5407  imadif  5442  imainlem  5443  fcoi1  5553  fcoi2  5554  f0rn0  5568  f1ocnv  5633  f1ocnvb  5634  fun11iun  5641  ffoss  5653  f1o00  5657  fo00  5658  relelfvdm  5708  nfvres  5712  nfunsn  5713  ssimaex  5744  fvmptss2  5758  fvmptssdm  5768  unpreima  5808  respreima  5811  elrnrexdm  5822  elrnrexdmb  5823  rexrnmpt  5826  dffo4  5831  rnmptss  5844  funiun  5865  funopdmsn  5870  fvpr1  5894  fvpr2  5895  elunirn  5946  f1veqaeq  5949  isores1  5994  iotaexel  6017  riotauni  6019  riotacl2  6027  riota1  6032  riota1a  6033  snriota  6044  eusvobj2  6045  acexmidlema  6050  acexmidlemb  6051  acexmidlem2  6056  oprabid  6091  0neqopab  6107  brabvv  6108  1stval2  6363  2ndval2  6364  xp1st  6373  xp2nd  6374  unielxp  6382  releldm2  6393  cnvf1o  6435  fo2ndf  6437  poxp  6442  reldmtpos  6498  dftpos4  6508  tpostpos  6509  tpostpos2  6510  iunon  6529  smoel  6545  tfrlem4  6558  tfrlem7  6562  tfrlem8  6563  tfrlem9  6564  nnaord  6756  ecexr  6786  swoord1  6810  swoord2  6811  0er  6815  mapprc  6900  mapsnconst  6943  ixpf  6969  mptelixpg  6983  idssen  7030  ener  7033  en0  7049  en1  7053  en1bg  7054  2dom  7060  modom  7075  enm  7085  xpsnen  7086  ssenen  7119  snnen2og  7127  php5dom  7131  phpm  7134  findcard  7159  findcard2  7160  findcard2s  7161  unfiexmid  7192  fiintim  7205  fidcenumlemim  7236  sbthlem1  7241  fiss  7278  djuexb  7349  djuss  7375  eldju2ndl  7377  eldju2ndr  7378  ctssdclemr  7417  exmidlpo  7448  finnum  7493  ficardon  7499  exmidfodomrlemim  7518  acnrcl  7522  3nsssucpw1  7560  indpi  7674  subhalfnqq  7746  archnqq  7749  enq0sym  7764  nqnq0pi  7770  nqnq0  7773  mulnnnq0  7782  prml  7809  prmu  7810  prssnql  7811  prssnqu  7812  prcdnql  7816  prcunqu  7817  prltlu  7819  prnmaxl  7820  prnminu  7821  prloc  7823  prdisj  7824  addcanprg  7948  recexprlemopl  7957  recexprlemopu  7959  cauappcvgprlemladdfu  7986  caucvgprlemladdfu  8009  recexgt0sr  8105  renfdisj  8350  axsuploc  8363  negf1o  8674  recexre  8871  apsqgt0  8894  apreim  8896  aprcl  8939  recexaplem2  8945  rerecclap  9025  nn0ge0  9542  elnnnn0b  9561  xnn0xr  9589  xnn0nemnf  9595  xnn0nnn0pnf  9597  znegcl  9629  zeo  9705  nn0ind  9714  nn0ind-raph  9717  uzn0  9892  eluzaddi  9903  eluzsubi  9904  uznn0sub  9908  uz3m2nn  9927  uznnssnn  9931  uz2m1nn  9959  uz2mulcl  9962  indstr2  9963  qmulz  9977  qre  9979  qnegcl  9990  qreccl  9996  rphalflt  10038  nn0ledivnn  10122  xrltnr  10135  nltpnft  10170  ngtmnft  10173  xrrebnd  10175  xnegcl  10188  xnegneg  10189  xltnegi  10191  xrpnfdc  10198  xrmnfdc  10199  xnegid  10215  xaddid1  10218  xnn0lenn0nn0  10221  xnn0xadd0  10223  xposdif  10238  elioore  10268  elfzuz2  10387  uzsubsubfz  10405  fzdisj  10410  fzmmmeqm  10417  elfz0ubfz0  10485  elfz0fzfz0  10486  fz0fzelfz0  10487  fz0fzdiffz0  10490  elfzmlbp  10492  difelfzle  10494  difelfznle  10495  nn0disj  10498  2ffzeq  10501  fzo1fzo0n0  10548  elfzo0z  10549  elfzo0le  10550  fzonmapblen  10552  fzofzim  10553  elfzodifsumelfzo  10572  elfzonlteqm1  10581  fzonn0p1p1  10584  elfzom1p1elfzo  10585  ssfzo12bi  10596  ubmelm1fzo  10597  fzind2  10611  subfzo0  10614  infssuzcldc  10621  rebtwn2z  10642  fldiv4p1lem1div2  10693  fldiv4lem1div2  10695  flqeqceilz  10708  zmodidfzoimp  10744  modfzo0difsn  10785  nnsinds  10835  nn0sinds  10836  expcl2lemap  10941  qexpclz  10950  zzlesq  11099  facp1  11121  facnn2  11125  faclbnd3  11134  bcn1  11149  hashfz0  11219  hashfibc  11236  wrdf  11259  swrdswrdlem  11425  swrdswrd  11426  swrdccatin1  11446  pfxccatin12lem2a  11448  pfxccatin12lem1  11449  swrdccatin2  11450  pfxccatin12lem2  11452  pfxccatin12lem3  11453  pfxccatin12  11454  pfxccat3  11455  swrdccat  11456  swrdccat3blem  11460  cvg1nlemres  11700  rexanuz  11703  fclim  12009  climmo  12013  iser3shft  12061  fsumsplitsn  12126  fsum2dlemstep  12150  fisumcom2  12154  arisum  12214  arisum2  12215  prodmodc  12294  fprodfac  12331  fprod2dlemstep  12338  fprodcom2fi  12342  fprodsplitsn  12349  eftlub  12406  ef01bndlem  12472  sin01gt0  12478  cos01gt0  12479  sin02gt0  12480  dvdsdivcl  12566  addmodlteqALT  12575  odd2np1  12589  oddge22np1  12597  m1expe  12615  nn0enne  12618  nn0o1gt2  12621  nno  12622  ndvdsadd  12647  dfgcd2  12740  mulgcd  12742  algfx  12779  prmind2  12847  prm2orodd  12853  prmgt1  12859  oddprmgt2  12861  dfphi2  12947  nnnn0modprm0  12983  prm23lt5  12991  pythagtriplem2  12994  pcz  13060  dvdsprmpweqnn  13064  oddprmdvds  13082  prmunb  13090  4sqlem4  13120  4sqlem19  13137  ballotfilem2  13177  ballotfilem7  13228  evenennn  13233  fngsum  13656  igsumvalx  13657  dfgrp3me  13860  mulgnn0gsum  13886  rngdi  14184  rngdir  14185  dvdsrcl2  14349  unitinvcl  14373  unitinvinv  14374  unitlinv  14376  unitrinv  14377  opprdrng  14563  rmodislmodlem  14629  rmodislmod  14630  zrhval  14896  psrbagf  14949  distop  15081  ntrss  15115  ssntr  15118  lmrcl  15188  txuni2  15252  txcn  15271  hmeocnvb  15314  xmetunirn  15354  blssioo  15549  divcnap  15561  cdivcncfap  15600  dedekindeulemlub  15616  dedekindicclemlub  15625  dvexp2  15708  elply2  15731  plyco  15755  pilem3  15779  sincosq1sgn  15822  sincosq2sgn  15823  sincosq3sgn  15824  sincosq4sgn  15825  sinq12gt0  15826  fsumdvdsmul  15990  zabsle1  16003  lgsdir2lem4  16035  gausslemma2dlem0f  16058  gausslemma2dlem1a  16062  gausslemma2dlem2  16066  gausslemma2dlem3  16067  gausslemma2dlem4  16068  2lgslem1a1  16090  2lgslem3  16105  2lgsoddprmlem3  16115  2lgsoddprm  16117  2sqlem2  16119  2sqlem10  16129  vtxvalprc  16181  iedgvalprc  16182  upgrex  16229  umgredg  16271  ausgrusgrben  16294  usgruspgrben  16312  usgrislfuspgrdom  16316  uhgr2edg  16332  uspgredg2v  16347  griedg0ssusgr  16377  subusgr  16401  wlkv  16452  wlk1walkdom  16485  trlsv  16510  trlf1  16514  clwwlk1loop  16525  clwwlkext2edg  16548  umgr2cwwkdifex  16551  clwwlknonex2lem2  16564  clwwlknonex2e  16566  eupthv  16572  eupth2lem3lem4fi  16599  konigsberglem5  16618  bj-pm2.18st  16663  bj-dcstab  16669  decidi  16708  sumdc2  16712  bj-charfunbi  16722  bdel  16756  bdssex  16813  bj-indind  16843  findset  16856  nninfall  16928  trirec0  16969  neap0mkv  16995