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  1941  sbalyz  2053  sbal1yz  2055  nfsb4t  2068  euex  2110  eumo0  2111  mor  2123  exmodc  2131  mo3h  2134  mopick  2159  moexexdc  2165  euexex  2166  2euex  2168  exists2  2178  eqcoms  2235  eleq2s  2327  nfcr  2376  necon3ai  2461  rexnalim  2531  dfrex2dc  2533  rexex  2588  rsp  2589  ralim  2601  rexim  2636  r19.32r  2689  r19.44av  2702  r19.45av  2703  gencl  2846  gencbvex  2861  gencbval  2863  vtoclgf  2873  vtoclg1f  2874  pm13.183  2955  elrabi  2970  eueq2dc  2990  eueq3dc  2991  mob2  2997  euxfr2dc  3002  reu3  3007  rmoim  3018  2rmorex  3023  sbcex  3051  sbcbi2  3093  ra5  3132  sseq1  3261  difdif  3344  dfss4st  3454  difindiss  3475  undif3ss  3482  dfrab3ss  3499  abvor0dc  3532  reldisj  3560  disjel  3563  inssdif0im  3576  uneqdifeqim  3595  r19.2m  3596  r19.2mOLD  3597  r19.3rm  3598  r19.9rmv  3601  rexm  3609  ralm  3613  raaanlem  3614  ifnefalse  3633  ifnotdc  3661  ifandc  3663  ifmdc  3665  nelpri  3713  nelprd  3715  prprc1  3800  difprsn2  3834  diftpsn3  3835  snsssn  3865  preqr2  3873  preq12b  3874  opthpr  3876  prneimg  3878  oprcl  3907  pwprss  3910  intmin4  3977  uniintabim  3986  dfiin2g  4024  iinss2  4044  iundif2ss  4057  disjnim  4099  disjnims  4100  invdisj  4102  disjiun  4104  brne0  4159  brm  4160  trel  4215  trss  4217  ssex  4247  bnd2  4286  abssexg  4295  exmidexmid  4309  rext  4331  unipw  4333  euabex  4341  mss  4342  exss  4343  copsexg  4360  opelopabsb  4378  pwssunim  4405  epelg  4411  sowlin  4441  sotritric  4445  elsuci  4524  sucprc  4533  reusv3  4581  ordon  4608  onsucmin  4629  onsucelsucr  4630  unon  4633  onsucelsucexmid  4652  setind  4661  setind2  4662  sucprcreg  4671  en2lp  4676  eunex  4683  ordsoexmid  4684  ordpwsucss  4689  tfi  4704  peano1  4716  peano2  4717  find  4721  0nelelxp  4778  opelxp  4779  elvvuni  4814  optocl  4826  ralxpf  4901  rexxpf  4902  relop  4905  breldm  4960  reldmm  4975  dmxpm  4977  elreldm  4983  dmrnssfld  5020  dmcosseq  5029  resabs1  5067  resima2  5072  issref  5145  asymref  5148  xpidtr  5153  trin2  5154  poirr2  5155  xpmlem  5183  dmxpss  5193  xp11m  5201  cnveqb  5218  dfco2a  5263  cores2  5275  coi2  5279  relcnvtr  5282  relresfld  5292  relcnvexb  5302  cnviinm  5304  iotauni  5325  iota1  5327  iota4  5332  iotam  5344  dffun8  5380  fununfun  5399  funcnvsn  5401  imadif  5436  imainlem  5437  fcoi1  5547  fcoi2  5548  f0rn0  5562  f1ocnv  5627  f1ocnvb  5628  fun11iun  5635  ffoss  5647  f1o00  5651  fo00  5652  relelfvdm  5702  nfvres  5706  nfunsn  5707  ssimaex  5738  fvmptss2  5752  fvmptssdm  5762  unpreima  5802  respreima  5805  elrnrexdm  5816  elrnrexdmb  5817  rexrnmpt  5820  dffo4  5825  rnmptss  5838  funiun  5859  funopdmsn  5864  fvpr1  5888  fvpr2  5889  elunirn  5939  f1veqaeq  5942  isores1  5987  iotaexel  6008  riotauni  6010  riotacl2  6018  riota1  6023  riota1a  6024  snriota  6035  eusvobj2  6036  acexmidlema  6041  acexmidlemb  6042  acexmidlem2  6047  oprabid  6082  0neqopab  6098  brabvv  6099  1stval2  6349  2ndval2  6350  xp1st  6359  xp2nd  6360  unielxp  6368  releldm2  6379  cnvf1o  6421  fo2ndf  6423  poxp  6428  reldmtpos  6484  dftpos4  6494  tpostpos  6495  tpostpos2  6496  iunon  6515  smoel  6531  tfrlem4  6544  tfrlem7  6548  tfrlem8  6549  tfrlem9  6550  nnaord  6742  ecexr  6772  swoord1  6796  swoord2  6797  0er  6801  mapprc  6886  mapsnconst  6929  ixpf  6955  mptelixpg  6969  idssen  7016  ener  7019  en0  7035  en1  7039  en1bg  7040  2dom  7046  modom  7061  enm  7071  xpsnen  7072  ssenen  7105  snnen2og  7113  php5dom  7117  phpm  7120  findcard  7145  findcard2  7146  findcard2s  7147  unfiexmid  7178  fiintim  7191  fidcenumlemim  7222  sbthlem1  7227  fiss  7264  djuexb  7335  djuss  7361  eldju2ndl  7363  eldju2ndr  7364  ctssdclemr  7403  exmidlpo  7434  finnum  7479  ficardon  7485  exmidfodomrlemim  7504  acnrcl  7508  3nsssucpw1  7546  indpi  7657  subhalfnqq  7729  archnqq  7732  enq0sym  7747  nqnq0pi  7753  nqnq0  7756  mulnnnq0  7765  prml  7792  prmu  7793  prssnql  7794  prssnqu  7795  prcdnql  7799  prcunqu  7800  prltlu  7802  prnmaxl  7803  prnminu  7804  prloc  7806  prdisj  7807  addcanprg  7931  recexprlemopl  7940  recexprlemopu  7942  cauappcvgprlemladdfu  7969  caucvgprlemladdfu  7992  recexgt0sr  8088  renfdisj  8333  axsuploc  8346  negf1o  8655  recexre  8852  apsqgt0  8875  apreim  8877  aprcl  8920  recexaplem2  8926  rerecclap  9004  nn0ge0  9521  elnnnn0b  9540  xnn0xr  9568  xnn0nemnf  9574  xnn0nnn0pnf  9576  znegcl  9608  zeo  9683  nn0ind  9692  nn0ind-raph  9695  uzn0  9870  eluzaddi  9881  eluzsubi  9882  uznn0sub  9886  uz3m2nn  9905  uznnssnn  9909  uz2m1nn  9937  uz2mulcl  9940  indstr2  9941  qmulz  9955  qre  9957  qnegcl  9968  qreccl  9974  rphalflt  10016  nn0ledivnn  10100  xrltnr  10112  nltpnft  10147  ngtmnft  10150  xrrebnd  10152  xnegcl  10165  xnegneg  10166  xltnegi  10168  xrpnfdc  10175  xrmnfdc  10176  xnegid  10192  xaddid1  10195  xnn0lenn0nn0  10198  xnn0xadd0  10200  xposdif  10215  elioore  10245  elfzuz2  10363  uzsubsubfz  10381  fzdisj  10386  fzmmmeqm  10392  elfz0ubfz0  10459  elfz0fzfz0  10460  fz0fzelfz0  10461  fz0fzdiffz0  10464  elfzmlbp  10466  difelfzle  10468  difelfznle  10469  nn0disj  10472  2ffzeq  10475  fzo1fzo0n0  10522  elfzo0z  10523  elfzo0le  10524  fzonmapblen  10526  fzofzim  10527  elfzodifsumelfzo  10546  elfzonlteqm1  10555  fzonn0p1p1  10558  elfzom1p1elfzo  10559  ssfzo12bi  10570  ubmelm1fzo  10571  fzind2  10585  subfzo0  10588  infssuzcldc  10595  rebtwn2z  10614  fldiv4p1lem1div2  10665  fldiv4lem1div2  10667  flqeqceilz  10680  zmodidfzoimp  10716  modfzo0difsn  10757  nnsinds  10807  nn0sinds  10808  expcl2lemap  10913  qexpclz  10922  zzlesq  11070  facp1  11092  facnn2  11096  faclbnd3  11105  bcn1  11120  hashfz0  11190  hashfibc  11207  wrdf  11230  swrdswrdlem  11396  swrdswrd  11397  swrdccatin1  11417  pfxccatin12lem2a  11419  pfxccatin12lem1  11420  swrdccatin2  11421  pfxccatin12lem2  11423  pfxccatin12lem3  11424  pfxccatin12  11425  pfxccat3  11426  swrdccat  11427  swrdccat3blem  11431  cvg1nlemres  11670  rexanuz  11673  fclim  11979  climmo  11983  iser3shft  12031  fsumsplitsn  12096  fsum2dlemstep  12120  fisumcom2  12124  arisum  12184  arisum2  12185  prodmodc  12264  fprodfac  12301  fprod2dlemstep  12308  fprodcom2fi  12312  fprodsplitsn  12319  eftlub  12376  ef01bndlem  12442  sin01gt0  12448  cos01gt0  12449  sin02gt0  12450  dvdsdivcl  12536  addmodlteqALT  12545  odd2np1  12559  oddge22np1  12567  m1expe  12585  nn0enne  12588  nn0o1gt2  12591  nno  12592  ndvdsadd  12617  dfgcd2  12710  mulgcd  12712  algfx  12749  prmind2  12817  prm2orodd  12823  prmgt1  12829  oddprmgt2  12831  dfphi2  12917  nnnn0modprm0  12953  prm23lt5  12961  pythagtriplem2  12964  pcz  13030  dvdsprmpweqnn  13034  oddprmdvds  13052  prmunb  13060  4sqlem4  13090  4sqlem19  13107  ballotfilem2  13142  evenennn  13144  fngsum  13601  igsumvalx  13602  dfgrp3me  13813  mulgnn0gsum  13845  rngdi  14084  rngdir  14085  dvdsrcl2  14244  unitinvcl  14268  unitinvinv  14269  unitlinv  14271  unitrinv  14272  rmodislmodlem  14498  rmodislmod  14499  zrhval  14765  psrbagf  14818  distop  14950  ntrss  14984  ssntr  14987  lmrcl  15057  txuni2  15121  txcn  15140  hmeocnvb  15183  xmetunirn  15223  blssioo  15418  divcnap  15430  cdivcncfap  15469  dedekindeulemlub  15485  dedekindicclemlub  15494  dvexp2  15577  elply2  15600  plyco  15624  pilem3  15648  sincosq1sgn  15691  sincosq2sgn  15692  sincosq3sgn  15693  sincosq4sgn  15694  sinq12gt0  15695  fsumdvdsmul  15859  zabsle1  15872  lgsdir2lem4  15904  gausslemma2dlem0f  15927  gausslemma2dlem1a  15931  gausslemma2dlem2  15935  gausslemma2dlem3  15936  gausslemma2dlem4  15937  2lgslem1a1  15959  2lgslem3  15974  2lgsoddprmlem3  15984  2lgsoddprm  15986  2sqlem2  15988  2sqlem10  15998  vtxvalprc  16050  iedgvalprc  16051  upgrex  16098  umgredg  16140  ausgrusgrben  16163  usgruspgrben  16181  usgrislfuspgrdom  16185  uhgr2edg  16201  uspgredg2v  16216  griedg0ssusgr  16246  subusgr  16270  wlkv  16321  wlk1walkdom  16354  trlsv  16379  trlf1  16383  clwwlk1loop  16394  clwwlkext2edg  16417  umgr2cwwkdifex  16420  clwwlknonex2lem2  16433  clwwlknonex2e  16435  eupthv  16441  eupth2lem3lem4fi  16468  konigsberglem5  16487  bj-pm2.18st  16522  bj-dcstab  16528  decidi  16567  sumdc2  16571  bj-charfunbi  16581  bdel  16615  bdssex  16672  bj-indind  16702  findset  16715  nninfall  16787  trirec0  16828  neap0mkv  16855