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 )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  sylbb  123  sylbb2  138  3imtr4i  201  simplbiim  391  mpan10  478  an12s  571  an32s  574  an4s  596  sylnbi  689  dcim  853  notnotrdc  855  condcOLD  866  pm2.61ddc  873  pm5.18dc  895  pm2.25dc  905  pm2.85dc  917  pm5.12dc  922  pm5.14dc  923  pm5.55dc  925  peircedc  926  pm5.54dc  930  dcand  945  dcor  948  pm5.62dc  958  pm5.63dc  959  pm4.83dc  964  ifp2  993  ifpor  1000  1fpid3  1007  3simpb  1026  3simpc  1027  3imp  1224  3com12  1238  3com13  1239  syl3anb  1321  xoranor  1426  xorbin  1433  xordc1  1442  biassdc  1444  nfr  1571  nfand  1621  19.21t  1635  19.30dc  1680  exintrbi  1686  19.9t  1695  nfnt  1708  equveli  1812  exdistrfor  1853  sbcof2  1863  sbidm  1904  sbi1v  1946  sbalyz  2059  sbal1yz  2061  nfsb4t  2074  euex  2116  eumo0  2117  mor  2129  exmodc  2137  mo3h  2140  mopick  2165  moexexdc  2171  euexex  2172  2euex  2174  exists2  2184  eqcoms  2241  eleq2s  2333  nfcr  2384  necon3ai  2469  rexnalim  2539  dfrex2dc  2541  rexex  2596  rsp  2597  ralim  2609  rexim  2644  r19.32r  2697  r19.44av  2710  r19.45av  2711  gencl  2854  gencbvex  2869  gencbval  2871  vtoclgf  2881  vtoclg1f  2882  pm13.183  2964  elrabi  2979  eueq2dc  2999  eueq3dc  3000  mob2  3006  euxfr2dc  3011  reu3  3016  rmoim  3027  2rmorex  3032  sbcex  3060  sbcbi2  3102  ra5  3141  sseq1  3271  difdif  3354  dfss4st  3464  difindiss  3485  undif3ss  3492  dfrab3ss  3511  abvor0dc  3545  reldisj  3576  disjel  3579  inssdif0imOLD  3593  uneqdifeqim  3613  r19.2m  3614  r19.2mOLD  3615  r19.3rm  3616  r19.9rmv  3619  rexm  3627  ralm  3631  raaanlem  3632  ifnefalse  3651  ifnotdc  3679  ifandc  3681  ifmdc  3683  nelpri  3733  nelprd  3735  prprc1  3821  difprsn2  3855  diftpsn3  3856  snsssn  3886  preqr2  3894  preq12b  3895  opthpr  3897  prneimg  3899  oprcl  3928  pwprss  3931  intmin4  3998  uniintabim  4007  dfiin2g  4045  iinss2  4065  iundif2ss  4078  disjnim  4120  disjnims  4121  invdisj  4123  disjiun  4125  brne0  4181  brm  4182  trel  4238  trss  4240  ssex  4272  bnd2  4312  abssexg  4321  exmidexmid  4335  rext  4357  unipw  4359  euabex  4367  mss  4368  exss  4369  copsexg  4386  opelopabsb  4404  pwssunim  4431  epelg  4437  sowlin  4467  sotritric  4471  elsuci  4550  sucprc  4559  reusv3  4608  ordon  4635  onsucmin  4656  onsucelsucr  4657  unon  4660  onsucelsucexmid  4679  setind  4688  setind2  4689  sucprcreg  4698  en2lp  4703  eunex  4710  ordsoexmid  4711  ordpwsucss  4716  tfi  4731  peano1  4743  peano2  4744  find  4748  0nelelxp  4805  opelxp  4806  elvvuni  4841  optocl  4853  ralxpf  4928  rexxpf  4929  relop  4932  breldm  4987  reldmm  5002  dmxpm  5004  elreldm  5010  dmrnssfld  5047  dmcosseq  5056  resabs1  5094  resima2  5099  issref  5173  asymref  5176  xpidtr  5181  trin2  5182  poirr2  5183  xpmlem  5211  dmxpss  5221  xp11m  5229  cnveqb  5246  dfco2a  5291  cores2  5303  coi2  5307  relcnvtr  5310  relresfld  5320  relcnvexb  5330  cnviinm  5332  iotauni  5353  iota1  5355  iota4  5360  iotam  5372  dffun8  5408  fununfun  5427  funcnvsn  5429  imadif  5464  imainlem  5465  fcoi1  5575  fcoi2  5576  f0rn0  5590  f1ocnv  5655  f1ocnvb  5656  fun11iun  5663  ffoss  5675  f1o00  5679  fo00  5680  relelfvdm  5730  nfvres  5735  nfunsn  5736  ssimaex  5767  fvmptss2  5783  fvmptssdm  5793  unpreima  5836  respreima  5839  elrnrexdm  5850  elrnrexdmb  5851  rexrnmpt  5854  dffo4  5859  rnmptss  5872  funiun  5893  funopdmsn  5898  fvpr1  5922  fvpr2  5923  elunirn  5975  f1veqaeq  5978  isores1  6023  iotaexel  6046  riotauni  6048  riotacl2  6056  riota1  6061  riota1a  6062  snriota  6073  eusvobj2  6074  acexmidlema  6079  acexmidlemb  6080  acexmidlem2  6085  oprabid  6120  0neqopab  6136  brabvv  6137  1stval2  6393  2ndval2  6394  xp1st  6403  xp2nd  6404  unielxp  6412  releldm2  6423  cnvf1o  6465  fo2ndf  6467  poxp  6472  reldmtpos  6528  dftpos4  6538  tpostpos  6539  tpostpos2  6540  iunon  6559  smoel  6575  tfrlem4  6588  tfrlem7  6592  tfrlem8  6593  tfrlem9  6594  nnaord  6786  ecexr  6816  swoord1  6840  swoord2  6841  0er  6845  mapprc  6930  mapfoss  6951  fsetdmprc0  6954  mapsnconst  6980  ixpf  7006  mptelixpg  7020  idssen  7067  ener  7070  en0  7086  en1  7090  en1bg  7091  2dom  7097  modom  7112  enm  7122  xpsnen  7123  ssenen  7156  snnen2og  7164  php5dom  7168  phpm  7171  findcard  7196  findcard2  7197  findcard2s  7198  unfiexmid  7229  fiintim  7242  fidcenumlemim  7274  sbthlem1  7279  fiss  7316  djuexb  7390  djuss  7416  eldju2ndl  7418  eldju2ndr  7419  ctssdclemr  7458  exmidlpo  7489  finnum  7534  ficardon  7540  exmidfodomrlemim  7559  acnrcl  7563  3nsssucpw1  7601  indpi  7715  subhalfnqq  7787  archnqq  7790  enq0sym  7805  nqnq0pi  7811  nqnq0  7814  mulnnnq0  7823  prml  7850  prmu  7851  prssnql  7852  prssnqu  7853  prcdnql  7857  prcunqu  7858  prltlu  7860  prnmaxl  7861  prnminu  7862  prloc  7864  prdisj  7865  addcanprg  7989  recexprlemopl  7998  recexprlemopu  8000  cauappcvgprlemladdfu  8027  caucvgprlemladdfu  8050  recexgt0sr  8146  renfdisj  8391  axsuploc  8404  negf1o  8716  recexre  8914  apsqgt0  8937  apreim  8939  aprcl  8982  recexaplem2  8988  rerecclap  9068  nn0ge0  9599  elnnnn0b  9618  xnn0xr  9646  xnn0nemnf  9652  xnn0nnn0pnf  9654  znegcl  9686  zeo  9762  nn0ind  9771  nn0ind-raph  9774  uzn0  9954  eluzaddi  9965  eluzsubi  9966  uznn0sub  9970  uz3m2nn  9989  uznnssnn  9993  uz2m1nn  10021  uz2mulcl  10024  indstr2  10025  qmulz  10039  qre  10041  qnegcl  10052  qreccl  10058  rphalflt  10101  nn0ledivnn  10185  xrltnr  10198  nltpnft  10233  ngtmnft  10236  xrrebnd  10238  xnegcl  10251  xnegneg  10252  xltnegi  10254  xrpnfdc  10261  xrmnfdc  10262  xnegid  10278  xaddid1  10281  xnn0lenn0nn0  10284  xnn0xadd0  10286  xposdif  10301  elioore  10331  elfzuz2  10450  uzsubsubfz  10469  fzdisj  10474  fzmmmeqm  10481  elfz0ubfz0  10549  elfz0fzfz0  10550  fz0fzelfz0  10551  fz0fzdiffz0  10554  elfzmlbp  10556  difelfzle  10558  difelfznle  10559  nn0disj  10562  2ffzeq  10565  fzo1fzo0n0  10612  elfzo0z  10613  elfzo0le  10614  fzonmapblen  10616  fzofzim  10617  elfzodifsumelfzo  10636  elfzonlteqm1  10645  fzonn0p1p1  10648  elfzom1p1elfzo  10649  ssfzo12bi  10660  ubmelm1fzo  10661  fzind2  10675  subfzo0  10678  infssuzcldc  10685  rebtwn2z  10706  fldiv4p1lem1div2  10761  fldiv4lem1div2  10763  flqeqceilz  10776  zmodidfzoimp  10812  modfzo0difsn  10853  nnsinds  10903  nn0sinds  10904  expcl2lemap  11009  qexpclz  11018  zzlesq  11167  facp1  11190  facnn2  11194  faclbnd3  11203  bcn1  11218  hashfz0  11288  hashfibc  11305  hashf1lem2  11308  wrdf  11332  swrdswrdlem  11498  swrdswrd  11499  swrdccatin1  11519  pfxccatin12lem2a  11521  pfxccatin12lem1  11522  swrdccatin2  11523  pfxccatin12lem2  11525  pfxccatin12lem3  11526  pfxccatin12  11527  pfxccat3  11528  swrdccat  11529  swrdccat3blem  11533  cvg1nlemres  11773  rexanuz  11776  fclim  12085  climmo  12089  iser3shft  12137  fsumsplitsn  12202  fsum2dlemstep  12226  fisumcom2  12230  arisum  12290  arisum2  12291  prodmodc  12370  fprodfac  12407  fprod2dlemstep  12414  fprodcom2fi  12418  fprodsplitsn  12425  eftlub  12482  ef01bndlem  12548  sin01gt0  12554  cos01gt0  12555  sin02gt0  12556  dvdsdivcl  12642  addmodlteqALT  12651  odd2np1  12665  oddge22np1  12673  m1expe  12691  nn0enne  12694  nn0o1gt2  12697  nno  12698  ndvdsadd  12723  dfgcd2  12816  mulgcd  12818  algfx  12855  prmind2  12923  prm2orodd  12929  prmgt1  12936  oddprmgt2  12938  dfphi2  13027  nnnn0modprm0  13063  prm23lt5  13071  pythagtriplem2  13074  pcz  13140  dvdsprmpweqnn  13144  oddprmdvds  13162  prmunb  13170  4sqlem4  13200  4sqlem19  13217  ballotfilem2  13286  ballotfilem7  13337  evenennn  13342  fngzsum  13767  gzsumvalx  13768  dfgrp3me  13964  mulgnn0gzsum  13990  rngdi  14346  rngdir  14347  dvdsrcl2  14515  unitinvcl  14539  unitinvinv  14540  unitlinv  14542  unitrinv  14543  opprdrng  14729  rmodislmodlem  14796  rmodislmod  14797  zrhval  15061  psrbagf  15163  distop  15311  ntrss  15345  ssntr  15348  lmrcl  15418  txuni2  15482  txcn  15501  hmeocnvb  15544  xmetunirn  15584  blssioo  15779  divcnap  15791  cdivcncfap  15830  dedekindeulemlub  15846  dedekindicclemlub  15855  dvexp2  15938  elply2  15961  plyco  15985  pilem3  16010  sincosq1sgn  16053  sincosq2sgn  16054  sincosq3sgn  16055  sincosq4sgn  16056  sinq12gt0  16057  logfac  16126  birthdaylem1g  16225  fsumdvdsmul  16285  bpos1  16310  zabsle1  16323  lgsdir2lem4  16355  gausslemma2dlem0f  16378  gausslemma2dlem1a  16382  gausslemma2dlem2  16386  gausslemma2dlem3  16387  gausslemma2dlem4  16388  2lgslem1a1  16410  2lgslem3  16425  2lgsoddprmlem3  16435  2lgsoddprm  16437  2sqlem2  16439  2sqlem10  16449  vtxvalprc  16501  iedgvalprc  16502  upgrex  16549  umgredg  16591  ausgrusgrben  16614  usgruspgrben  16632  usgrislfuspgrdom  16636  uhgr2edg  16652  uspgredg2v  16667  griedg0ssusgr  16697  subusgr  16721  wlkv  16772  wlk1walkdom  16805  trlsv  16830  trlf1  16834  clwwlk1loop  16845  clwwlkext2edg  16868  umgr2cwwkdifex  16871  clwwlknonex2lem2  16884  clwwlknonex2e  16886  eupthv  16892  eupth2lem3lem4fi  16919  konigsberglem5  16938  bj-pm2.18st  16983  bj-dcstab  16989  decidi  17028  sumdc2  17032  bj-charfunbi  17042  bdel  17076  bdssex  17133  bj-indind  17163  findset  17176  wexmiddc  17247  wexmiddifxy  17251  idjudju  17252  nninfall  17258  trirec0  17300  neap0mkv  17326  alsex  17346  ralsex  17347