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  4180  brm  4181  trel  4236  trss  4238  ssex  4270  bnd2  4310  abssexg  4319  exmidexmid  4333  rext  4355  unipw  4357  euabex  4365  mss  4366  exss  4367  copsexg  4384  opelopabsb  4402  pwssunim  4429  epelg  4435  sowlin  4465  sotritric  4469  elsuci  4548  sucprc  4557  reusv3  4606  ordon  4633  onsucmin  4654  onsucelsucr  4655  unon  4658  onsucelsucexmid  4677  setind  4686  setind2  4687  sucprcreg  4696  en2lp  4701  eunex  4708  ordsoexmid  4709  ordpwsucss  4714  tfi  4729  peano1  4741  peano2  4742  find  4746  0nelelxp  4803  opelxp  4804  elvvuni  4839  optocl  4851  ralxpf  4926  rexxpf  4927  relop  4930  breldm  4985  reldmm  5000  dmxpm  5002  elreldm  5008  dmrnssfld  5045  dmcosseq  5054  resabs1  5092  resima2  5097  issref  5170  asymref  5173  xpidtr  5178  trin2  5179  poirr2  5180  xpmlem  5208  dmxpss  5218  xp11m  5226  cnveqb  5243  dfco2a  5288  cores2  5300  coi2  5304  relcnvtr  5307  relresfld  5317  relcnvexb  5327  cnviinm  5329  iotauni  5350  iota1  5352  iota4  5357  iotam  5369  dffun8  5405  fununfun  5424  funcnvsn  5426  imadif  5461  imainlem  5462  fcoi1  5572  fcoi2  5573  f0rn0  5587  f1ocnv  5652  f1ocnvb  5653  fun11iun  5660  ffoss  5672  f1o00  5676  fo00  5677  relelfvdm  5727  nfvres  5732  nfunsn  5733  ssimaex  5764  fvmptss2  5780  fvmptssdm  5790  unpreima  5833  respreima  5836  elrnrexdm  5847  elrnrexdmb  5848  rexrnmpt  5851  dffo4  5856  rnmptss  5869  funiun  5890  funopdmsn  5895  fvpr1  5919  fvpr2  5920  elunirn  5972  f1veqaeq  5975  isores1  6020  iotaexel  6043  riotauni  6045  riotacl2  6053  riota1  6058  riota1a  6059  snriota  6070  eusvobj2  6071  acexmidlema  6076  acexmidlemb  6077  acexmidlem2  6082  oprabid  6117  0neqopab  6133  brabvv  6134  1stval2  6389  2ndval2  6390  xp1st  6399  xp2nd  6400  unielxp  6408  releldm2  6419  cnvf1o  6461  fo2ndf  6463  poxp  6468  reldmtpos  6524  dftpos4  6534  tpostpos  6535  tpostpos2  6536  iunon  6555  smoel  6571  tfrlem4  6584  tfrlem7  6588  tfrlem8  6589  tfrlem9  6590  nnaord  6782  ecexr  6812  swoord1  6836  swoord2  6837  0er  6841  mapprc  6926  mapfoss  6947  fsetdmprc0  6950  mapsnconst  6976  ixpf  7002  mptelixpg  7016  idssen  7063  ener  7066  en0  7082  en1  7086  en1bg  7087  2dom  7093  modom  7108  enm  7118  xpsnen  7119  ssenen  7152  snnen2og  7160  php5dom  7164  phpm  7167  findcard  7192  findcard2  7193  findcard2s  7194  unfiexmid  7225  fiintim  7238  fidcenumlemim  7269  sbthlem1  7274  fiss  7311  djuexb  7384  djuss  7410  eldju2ndl  7412  eldju2ndr  7413  ctssdclemr  7452  exmidlpo  7483  finnum  7528  ficardon  7534  exmidfodomrlemim  7553  acnrcl  7557  3nsssucpw1  7595  indpi  7709  subhalfnqq  7781  archnqq  7784  enq0sym  7799  nqnq0pi  7805  nqnq0  7808  mulnnnq0  7817  prml  7844  prmu  7845  prssnql  7846  prssnqu  7847  prcdnql  7851  prcunqu  7852  prltlu  7854  prnmaxl  7855  prnminu  7856  prloc  7858  prdisj  7859  addcanprg  7983  recexprlemopl  7992  recexprlemopu  7994  cauappcvgprlemladdfu  8021  caucvgprlemladdfu  8044  recexgt0sr  8140  renfdisj  8385  axsuploc  8398  negf1o  8710  recexre  8908  apsqgt0  8931  apreim  8933  aprcl  8976  recexaplem2  8982  rerecclap  9062  nn0ge0  9592  elnnnn0b  9611  xnn0xr  9639  xnn0nemnf  9645  xnn0nnn0pnf  9647  znegcl  9679  zeo  9755  nn0ind  9764  nn0ind-raph  9767  uzn0  9947  eluzaddi  9958  eluzsubi  9959  uznn0sub  9963  uz3m2nn  9982  uznnssnn  9986  uz2m1nn  10014  uz2mulcl  10017  indstr2  10018  qmulz  10032  qre  10034  qnegcl  10045  qreccl  10051  rphalflt  10094  nn0ledivnn  10178  xrltnr  10191  nltpnft  10226  ngtmnft  10229  xrrebnd  10231  xnegcl  10244  xnegneg  10245  xltnegi  10247  xrpnfdc  10254  xrmnfdc  10255  xnegid  10271  xaddid1  10274  xnn0lenn0nn0  10277  xnn0xadd0  10279  xposdif  10294  elioore  10324  elfzuz2  10443  uzsubsubfz  10462  fzdisj  10467  fzmmmeqm  10474  elfz0ubfz0  10542  elfz0fzfz0  10543  fz0fzelfz0  10544  fz0fzdiffz0  10547  elfzmlbp  10549  difelfzle  10551  difelfznle  10552  nn0disj  10555  2ffzeq  10558  fzo1fzo0n0  10605  elfzo0z  10606  elfzo0le  10607  fzonmapblen  10609  fzofzim  10610  elfzodifsumelfzo  10629  elfzonlteqm1  10638  fzonn0p1p1  10641  elfzom1p1elfzo  10642  ssfzo12bi  10653  ubmelm1fzo  10654  fzind2  10668  subfzo0  10671  infssuzcldc  10678  rebtwn2z  10699  fldiv4p1lem1div2  10753  fldiv4lem1div2  10755  flqeqceilz  10768  zmodidfzoimp  10804  modfzo0difsn  10845  nnsinds  10895  nn0sinds  10896  expcl2lemap  11001  qexpclz  11010  zzlesq  11159  facp1  11182  facnn2  11186  faclbnd3  11195  bcn1  11210  hashfz0  11280  hashfibc  11297  hashf1lem2  11300  wrdf  11324  swrdswrdlem  11490  swrdswrd  11491  swrdccatin1  11511  pfxccatin12lem2a  11513  pfxccatin12lem1  11514  swrdccatin2  11515  pfxccatin12lem2  11517  pfxccatin12lem3  11518  pfxccatin12  11519  pfxccat3  11520  swrdccat  11521  swrdccat3blem  11525  cvg1nlemres  11765  rexanuz  11768  fclim  12076  climmo  12080  iser3shft  12128  fsumsplitsn  12193  fsum2dlemstep  12217  fisumcom2  12221  arisum  12281  arisum2  12282  prodmodc  12361  fprodfac  12398  fprod2dlemstep  12405  fprodcom2fi  12409  fprodsplitsn  12416  eftlub  12473  ef01bndlem  12539  sin01gt0  12545  cos01gt0  12546  sin02gt0  12547  dvdsdivcl  12633  addmodlteqALT  12642  odd2np1  12656  oddge22np1  12664  m1expe  12682  nn0enne  12685  nn0o1gt2  12688  nno  12689  ndvdsadd  12714  dfgcd2  12807  mulgcd  12809  algfx  12846  prmind2  12914  prm2orodd  12920  prmgt1  12927  oddprmgt2  12929  dfphi2  13018  nnnn0modprm0  13054  prm23lt5  13062  pythagtriplem2  13065  pcz  13131  dvdsprmpweqnn  13135  oddprmdvds  13153  prmunb  13161  4sqlem4  13191  4sqlem19  13208  ballotfilem2  13277  ballotfilem7  13328  evenennn  13333  fngzsum  13757  gzsumvalx  13758  dfgrp3me  13954  mulgnn0gzsum  13980  rngdi  14288  rngdir  14289  dvdsrcl2  14455  unitinvcl  14479  unitinvinv  14480  unitlinv  14482  unitrinv  14483  opprdrng  14669  rmodislmodlem  14736  rmodislmod  14737  zrhval  15001  psrbagf  15103  distop  15235  ntrss  15269  ssntr  15272  lmrcl  15342  txuni2  15406  txcn  15425  hmeocnvb  15468  xmetunirn  15508  blssioo  15703  divcnap  15715  cdivcncfap  15754  dedekindeulemlub  15770  dedekindicclemlub  15779  dvexp2  15862  elply2  15885  plyco  15909  pilem3  15934  sincosq1sgn  15977  sincosq2sgn  15978  sincosq3sgn  15979  sincosq4sgn  15980  sinq12gt0  15981  logfac  16048  birthdaylem1g  16144  fsumdvdsmul  16186  bpos1  16208  zabsle1  16216  lgsdir2lem4  16248  gausslemma2dlem0f  16271  gausslemma2dlem1a  16275  gausslemma2dlem2  16279  gausslemma2dlem3  16280  gausslemma2dlem4  16281  2lgslem1a1  16303  2lgslem3  16318  2lgsoddprmlem3  16328  2lgsoddprm  16330  2sqlem2  16332  2sqlem10  16342  vtxvalprc  16394  iedgvalprc  16395  upgrex  16442  umgredg  16484  ausgrusgrben  16507  usgruspgrben  16525  usgrislfuspgrdom  16529  uhgr2edg  16545  uspgredg2v  16560  griedg0ssusgr  16590  subusgr  16614  wlkv  16665  wlk1walkdom  16698  trlsv  16723  trlf1  16727  clwwlk1loop  16738  clwwlkext2edg  16761  umgr2cwwkdifex  16764  clwwlknonex2lem2  16777  clwwlknonex2e  16779  eupthv  16785  eupth2lem3lem4fi  16812  konigsberglem5  16831  bj-pm2.18st  16876  bj-dcstab  16882  decidi  16921  sumdc2  16925  bj-charfunbi  16935  bdel  16969  bdssex  17026  bj-indind  17056  findset  17069  wexmiddc  17140  wexmiddifxy  17144  nninfall  17150  trirec0  17191  neap0mkv  17217  alsex  17237  ralsex  17238