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  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  3575  disjel  3578  inssdif0im  3591  uneqdifeqim  3610  r19.2m  3611  r19.2mOLD  3612  r19.3rm  3613  r19.9rmv  3616  rexm  3624  ralm  3628  raaanlem  3629  ifnefalse  3648  ifnotdc  3676  ifandc  3678  ifmdc  3680  nelpri  3729  nelprd  3731  prprc1  3816  difprsn2  3850  diftpsn3  3851  snsssn  3881  preqr2  3889  preq12b  3890  opthpr  3892  prneimg  3894  oprcl  3923  pwprss  3926  intmin4  3993  uniintabim  4002  dfiin2g  4040  iinss2  4060  iundif2ss  4073  disjnim  4115  disjnims  4116  invdisj  4118  disjiun  4120  brne0  4175  brm  4176  trel  4231  trss  4233  ssex  4265  bnd2  4305  abssexg  4314  exmidexmid  4328  rext  4350  unipw  4352  euabex  4360  mss  4361  exss  4362  copsexg  4379  opelopabsb  4397  pwssunim  4424  epelg  4430  sowlin  4460  sotritric  4464  elsuci  4543  sucprc  4552  reusv3  4601  ordon  4628  onsucmin  4649  onsucelsucr  4650  unon  4653  onsucelsucexmid  4672  setind  4681  setind2  4682  sucprcreg  4691  en2lp  4696  eunex  4703  ordsoexmid  4704  ordpwsucss  4709  tfi  4724  peano1  4736  peano2  4737  find  4741  0nelelxp  4798  opelxp  4799  elvvuni  4834  optocl  4846  ralxpf  4921  rexxpf  4922  relop  4925  breldm  4980  reldmm  4995  dmxpm  4997  elreldm  5003  dmrnssfld  5040  dmcosseq  5049  resabs1  5087  resima2  5092  issref  5165  asymref  5168  xpidtr  5173  trin2  5174  poirr2  5175  xpmlem  5203  dmxpss  5213  xp11m  5221  cnveqb  5238  dfco2a  5283  cores2  5295  coi2  5299  relcnvtr  5302  relresfld  5312  relcnvexb  5322  cnviinm  5324  iotauni  5345  iota1  5347  iota4  5352  iotam  5364  dffun8  5400  fununfun  5419  funcnvsn  5421  imadif  5456  imainlem  5457  fcoi1  5567  fcoi2  5568  f0rn0  5582  f1ocnv  5647  f1ocnvb  5648  fun11iun  5655  ffoss  5667  f1o00  5671  fo00  5672  relelfvdm  5722  nfvres  5726  nfunsn  5727  ssimaex  5758  fvmptss2  5774  fvmptssdm  5784  unpreima  5824  respreima  5827  elrnrexdm  5838  elrnrexdmb  5839  rexrnmpt  5842  dffo4  5847  rnmptss  5860  funiun  5881  funopdmsn  5886  fvpr1  5910  fvpr2  5911  elunirn  5962  f1veqaeq  5965  isores1  6010  iotaexel  6033  riotauni  6035  riotacl2  6043  riota1  6048  riota1a  6049  snriota  6060  eusvobj2  6061  acexmidlema  6066  acexmidlemb  6067  acexmidlem2  6072  oprabid  6107  0neqopab  6123  brabvv  6124  1stval2  6379  2ndval2  6380  xp1st  6389  xp2nd  6390  unielxp  6398  releldm2  6409  cnvf1o  6451  fo2ndf  6453  poxp  6458  reldmtpos  6514  dftpos4  6524  tpostpos  6525  tpostpos2  6526  iunon  6545  smoel  6561  tfrlem4  6574  tfrlem7  6578  tfrlem8  6579  tfrlem9  6580  nnaord  6772  ecexr  6802  swoord1  6826  swoord2  6827  0er  6831  mapprc  6916  mapfoss  6937  fsetdmprc0  6940  mapsnconst  6966  ixpf  6992  mptelixpg  7006  idssen  7053  ener  7056  en0  7072  en1  7076  en1bg  7077  2dom  7083  modom  7098  enm  7108  xpsnen  7109  ssenen  7142  snnen2og  7150  php5dom  7154  phpm  7157  findcard  7182  findcard2  7183  findcard2s  7184  unfiexmid  7215  fiintim  7228  fidcenumlemim  7259  sbthlem1  7264  fiss  7301  djuexb  7374  djuss  7400  eldju2ndl  7402  eldju2ndr  7403  ctssdclemr  7442  exmidlpo  7473  finnum  7518  ficardon  7524  exmidfodomrlemim  7543  acnrcl  7547  3nsssucpw1  7585  indpi  7699  subhalfnqq  7771  archnqq  7774  enq0sym  7789  nqnq0pi  7795  nqnq0  7798  mulnnnq0  7807  prml  7834  prmu  7835  prssnql  7836  prssnqu  7837  prcdnql  7841  prcunqu  7842  prltlu  7844  prnmaxl  7845  prnminu  7846  prloc  7848  prdisj  7849  addcanprg  7973  recexprlemopl  7982  recexprlemopu  7984  cauappcvgprlemladdfu  8011  caucvgprlemladdfu  8034  recexgt0sr  8130  renfdisj  8375  axsuploc  8388  negf1o  8699  recexre  8896  apsqgt0  8919  apreim  8921  aprcl  8964  recexaplem2  8970  rerecclap  9050  nn0ge0  9567  elnnnn0b  9586  xnn0xr  9614  xnn0nemnf  9620  xnn0nnn0pnf  9622  znegcl  9654  zeo  9730  nn0ind  9739  nn0ind-raph  9742  uzn0  9917  eluzaddi  9928  eluzsubi  9929  uznn0sub  9933  uz3m2nn  9952  uznnssnn  9956  uz2m1nn  9984  uz2mulcl  9987  indstr2  9988  qmulz  10002  qre  10004  qnegcl  10015  qreccl  10021  rphalflt  10063  nn0ledivnn  10147  xrltnr  10160  nltpnft  10195  ngtmnft  10198  xrrebnd  10200  xnegcl  10213  xnegneg  10214  xltnegi  10216  xrpnfdc  10223  xrmnfdc  10224  xnegid  10240  xaddid1  10243  xnn0lenn0nn0  10246  xnn0xadd0  10248  xposdif  10263  elioore  10293  elfzuz2  10412  uzsubsubfz  10430  fzdisj  10435  fzmmmeqm  10442  elfz0ubfz0  10510  elfz0fzfz0  10511  fz0fzelfz0  10512  fz0fzdiffz0  10515  elfzmlbp  10517  difelfzle  10519  difelfznle  10520  nn0disj  10523  2ffzeq  10526  fzo1fzo0n0  10573  elfzo0z  10574  elfzo0le  10575  fzonmapblen  10577  fzofzim  10578  elfzodifsumelfzo  10597  elfzonlteqm1  10606  fzonn0p1p1  10609  elfzom1p1elfzo  10610  ssfzo12bi  10621  ubmelm1fzo  10622  fzind2  10636  subfzo0  10639  infssuzcldc  10646  rebtwn2z  10667  fldiv4p1lem1div2  10718  fldiv4lem1div2  10720  flqeqceilz  10733  zmodidfzoimp  10769  modfzo0difsn  10810  nnsinds  10860  nn0sinds  10861  expcl2lemap  10966  qexpclz  10975  zzlesq  11124  facp1  11146  facnn2  11150  faclbnd3  11159  bcn1  11174  hashfz0  11244  hashfibc  11261  hashf1lem2  11264  wrdf  11288  swrdswrdlem  11454  swrdswrd  11455  swrdccatin1  11475  pfxccatin12lem2a  11477  pfxccatin12lem1  11478  swrdccatin2  11479  pfxccatin12lem2  11481  pfxccatin12lem3  11482  pfxccatin12  11483  pfxccat3  11484  swrdccat  11485  swrdccat3blem  11489  cvg1nlemres  11729  rexanuz  11732  fclim  12038  climmo  12042  iser3shft  12090  fsumsplitsn  12155  fsum2dlemstep  12179  fisumcom2  12183  arisum  12243  arisum2  12244  prodmodc  12323  fprodfac  12360  fprod2dlemstep  12367  fprodcom2fi  12371  fprodsplitsn  12378  eftlub  12435  ef01bndlem  12501  sin01gt0  12507  cos01gt0  12508  sin02gt0  12509  dvdsdivcl  12595  addmodlteqALT  12604  odd2np1  12618  oddge22np1  12626  m1expe  12644  nn0enne  12647  nn0o1gt2  12650  nno  12651  ndvdsadd  12676  dfgcd2  12769  mulgcd  12771  algfx  12808  prmind2  12876  prm2orodd  12882  prmgt1  12888  oddprmgt2  12890  dfphi2  12976  nnnn0modprm0  13012  prm23lt5  13020  pythagtriplem2  13023  pcz  13089  dvdsprmpweqnn  13093  oddprmdvds  13111  prmunb  13119  4sqlem4  13149  4sqlem19  13166  ballotfilem2  13206  ballotfilem7  13257  evenennn  13262  fngzsum  13685  gzsumvalx  13686  dfgrp3me  13882  mulgnn0gzsum  13908  rngdi  14214  rngdir  14215  dvdsrcl2  14379  unitinvcl  14403  unitinvinv  14404  unitlinv  14406  unitrinv  14407  opprdrng  14593  rmodislmodlem  14659  rmodislmod  14660  zrhval  14924  psrbagf  14977  distop  15109  ntrss  15143  ssntr  15146  lmrcl  15216  txuni2  15280  txcn  15299  hmeocnvb  15342  xmetunirn  15382  blssioo  15577  divcnap  15589  cdivcncfap  15628  dedekindeulemlub  15644  dedekindicclemlub  15653  dvexp2  15736  elply2  15759  plyco  15783  pilem3  15807  sincosq1sgn  15850  sincosq2sgn  15851  sincosq3sgn  15852  sincosq4sgn  15853  sinq12gt0  15854  logfac  15918  fsumdvdsmul  16019  zabsle1  16032  lgsdir2lem4  16064  gausslemma2dlem0f  16087  gausslemma2dlem1a  16091  gausslemma2dlem2  16095  gausslemma2dlem3  16096  gausslemma2dlem4  16097  2lgslem1a1  16119  2lgslem3  16134  2lgsoddprmlem3  16144  2lgsoddprm  16146  2sqlem2  16148  2sqlem10  16158  vtxvalprc  16210  iedgvalprc  16211  upgrex  16258  umgredg  16300  ausgrusgrben  16323  usgruspgrben  16341  usgrislfuspgrdom  16345  uhgr2edg  16361  uspgredg2v  16376  griedg0ssusgr  16406  subusgr  16430  wlkv  16481  wlk1walkdom  16514  trlsv  16539  trlf1  16543  clwwlk1loop  16554  clwwlkext2edg  16577  umgr2cwwkdifex  16580  clwwlknonex2lem2  16593  clwwlknonex2e  16595  eupthv  16601  eupth2lem3lem4fi  16628  konigsberglem5  16647  bj-pm2.18st  16692  bj-dcstab  16698  decidi  16737  sumdc2  16741  bj-charfunbi  16751  bdel  16785  bdssex  16842  bj-indind  16872  findset  16885  nninfall  16957  trirec0  16998  neap0mkv  17024