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  6529  dftpos4  6539  tpostpos  6540  tpostpos2  6541  iunon  6560  smoel  6576  tfrlem4  6589  tfrlem7  6593  tfrlem8  6594  tfrlem9  6595  nnaord  6787  ecexr  6817  swoord1  6841  swoord2  6842  0er  6846  mapprc  6931  mapfoss  6952  fsetdmprc0  6955  mapsnconst  6982  ixpf  7008  mptelixpg  7022  idssen  7069  ener  7072  en0  7088  en1  7092  en1bg  7093  2dom  7099  modom  7114  enm  7124  xpsnen  7125  ssenen  7158  snnen2og  7166  php5dom  7170  phpm  7173  findcard  7198  findcard2  7199  findcard2s  7200  unfiexmid  7231  fiintim  7244  fidcenumlemim  7276  sbthlem1  7281  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  9644  xnn0nemnf  9650  xnn0nnn0pnf  9652  znegcl  9684  zeo  9761  nn0ind  9770  nn0ind-raph  9773  uzn0  9953  eluzaddi  9964  eluzsubi  9965  uznn0sub  9969  uz3m2nn  9988  uznnssnn  9992  uz2m1nn  10020  uz2mulcl  10023  indstr2  10024  qmulz  10038  qre  10040  qnegcl  10051  qreccl  10057  rphalflt  10100  nn0ledivnn  10184  xrltnr  10197  nltpnft  10232  ngtmnft  10235  xrrebnd  10237  xnegcl  10250  xnegneg  10251  xltnegi  10253  xrpnfdc  10260  xrmnfdc  10261  xnegid  10277  xaddid1  10280  xnn0lenn0nn0  10283  xnn0xadd0  10285  xposdif  10300  elioore  10330  elfzuz2  10449  uzsubsubfz  10468  fzdisj  10473  fzmmmeqm  10480  elfz0ubfz0  10548  elfz0fzfz0  10549  fz0fzelfz0  10550  fz0fzdiffz0  10553  elfzmlbp  10555  difelfzle  10557  difelfznle  10558  nn0disj  10561  2ffzeq  10564  fzo1fzo0n0  10611  elfzo0z  10612  elfzo0le  10613  fzonmapblen  10615  fzofzim  10616  elfzodifsumelfzo  10635  elfzonlteqm1  10644  fzonn0p1p1  10647  elfzom1p1elfzo  10648  ssfzo12bi  10659  ubmelm1fzo  10660  fzind2  10674  subfzo0  10677  infssuzcldc  10684  rebtwn2z  10705  fldiv4p1lem1div2  10760  fldiv4lem1div2  10762  flqeqceilz  10775  zmodidfzoimp  10811  modfzo0difsn  10852  nnsinds  10902  nn0sinds  10903  expcl2lemap  11008  qexpclz  11017  zzlesq  11166  facp1  11189  facnn2  11193  faclbnd3  11202  bcn1  11217  hashfz0  11287  hashfibc  11304  hashf1lem2  11307  wrdf  11331  swrdswrdlem  11497  swrdswrd  11498  swrdccatin1  11518  pfxccatin12lem2a  11520  pfxccatin12lem1  11521  swrdccatin2  11522  pfxccatin12lem2  11524  pfxccatin12lem3  11525  pfxccatin12  11526  pfxccat3  11527  swrdccat  11528  swrdccat3blem  11532  cvg1nlemres  11772  rexanuz  11775  fclim  12084  climmo  12088  iser3shft  12136  fsumsplitsn  12201  fsum2dlemstep  12225  fisumcom2  12229  arisum  12289  arisum2  12290  prodmodc  12369  fprodfac  12406  fprod2dlemstep  12413  fprodcom2fi  12417  fprodsplitsn  12424  eftlub  12481  ef01bndlem  12547  sin01gt0  12553  cos01gt0  12554  sin02gt0  12555  dvdsdivcl  12641  addmodlteqALT  12650  odd2np1  12664  oddge22np1  12672  m1expe  12690  nn0enne  12693  nn0o1gt2  12696  nno  12697  ndvdsadd  12722  dfgcd2  12815  mulgcd  12817  algfx  12854  prmind2  12922  prm2orodd  12928  prmgt1  12935  oddprmgt2  12937  dfphi2  13026  nnnn0modprm0  13062  prm23lt5  13070  pythagtriplem2  13073  pcz  13139  dvdsprmpweqnn  13143  oddprmdvds  13161  prmunb  13169  4sqlem4  13199  4sqlem19  13216  ballotfilem2  13285  ballotfilem7  13336  evenennn  13341  fngzsum  13766  gzsumvalx  13767  dfgrp3me  13963  mulgnn0gzsum  13989  rngdi  14345  rngdir  14346  dvdsrcl2  14514  unitinvcl  14538  unitinvinv  14539  unitlinv  14541  unitrinv  14542  opprdrng  14728  rmodislmodlem  14795  rmodislmod  14796  zrhval  15060  psrbagf  15164  distop  15328  ntrss  15362  ssntr  15365  lmrcl  15435  txuni2  15499  txcn  15518  hmeocnvb  15561  xmetunirn  15601  blssioo  15796  divcnap  15808  cdivcncfap  15847  dedekindeulemlub  15863  dedekindicclemlub  15872  dvexp2  15955  elply2  15978  plyco  16002  pilem3  16027  sincosq1sgn  16070  sincosq2sgn  16071  sincosq3sgn  16072  sincosq4sgn  16073  sinq12gt0  16074  logfac  16143  birthdaylem1g  16242  fsumdvdsmul  16302  bpos1  16327  zabsle1  16340  lgsdir2lem4  16372  gausslemma2dlem0f  16395  gausslemma2dlem1a  16399  gausslemma2dlem2  16403  gausslemma2dlem3  16404  gausslemma2dlem4  16405  2lgslem1a1  16427  2lgslem3  16442  2lgsoddprmlem3  16452  2lgsoddprm  16454  2sqlem2  16456  2sqlem10  16466  vtxvalprc  16518  iedgvalprc  16519  upgrex  16566  umgredg  16608  ausgrusgrben  16631  usgruspgrben  16649  usgrislfuspgrdom  16653  uhgr2edg  16669  uspgredg2v  16684  griedg0ssusgr  16714  subusgr  16738  wlkv  16789  wlk1walkdom  16822  trlsv  16847  trlf1  16851  clwwlk1loop  16862  clwwlkext2edg  16885  umgr2cwwkdifex  16888  clwwlknonex2lem2  16901  clwwlknonex2e  16903  eupthv  16909  eupth2lem3lem4fi  16936  konigsberglem5  16955  bj-pm2.18st  17000  bj-dcstab  17006  decidi  17045  sumdc2  17049  bj-charfunbi  17059  bdel  17093  bdssex  17150  bj-indind  17180  findset  17193  wexmiddc  17264  wexmiddifxy  17268  idjudju  17269  nninfall  17275  trirec0  17317  neap0mkv  17343  alsex  17363  ralsex  17364