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  8709  recexre  8906  apsqgt0  8929  apreim  8931  aprcl  8974  recexaplem2  8980  rerecclap  9060  nn0ge0  9588  elnnnn0b  9607  xnn0xr  9635  xnn0nemnf  9641  xnn0nnn0pnf  9643  znegcl  9675  zeo  9751  nn0ind  9760  nn0ind-raph  9763  uzn0  9938  eluzaddi  9949  eluzsubi  9950  uznn0sub  9954  uz3m2nn  9973  uznnssnn  9977  uz2m1nn  10005  uz2mulcl  10008  indstr2  10009  qmulz  10023  qre  10025  qnegcl  10036  qreccl  10042  rphalflt  10084  nn0ledivnn  10168  xrltnr  10181  nltpnft  10216  ngtmnft  10219  xrrebnd  10221  xnegcl  10234  xnegneg  10235  xltnegi  10237  xrpnfdc  10244  xrmnfdc  10245  xnegid  10261  xaddid1  10264  xnn0lenn0nn0  10267  xnn0xadd0  10269  xposdif  10284  elioore  10314  elfzuz2  10433  uzsubsubfz  10452  fzdisj  10457  fzmmmeqm  10464  elfz0ubfz0  10532  elfz0fzfz0  10533  fz0fzelfz0  10534  fz0fzdiffz0  10537  elfzmlbp  10539  difelfzle  10541  difelfznle  10542  nn0disj  10545  2ffzeq  10548  fzo1fzo0n0  10595  elfzo0z  10596  elfzo0le  10597  fzonmapblen  10599  fzofzim  10600  elfzodifsumelfzo  10619  elfzonlteqm1  10628  fzonn0p1p1  10631  elfzom1p1elfzo  10632  ssfzo12bi  10643  ubmelm1fzo  10644  fzind2  10658  subfzo0  10661  infssuzcldc  10668  rebtwn2z  10689  fldiv4p1lem1div2  10740  fldiv4lem1div2  10742  flqeqceilz  10755  zmodidfzoimp  10791  modfzo0difsn  10832  nnsinds  10882  nn0sinds  10883  expcl2lemap  10988  qexpclz  10997  zzlesq  11146  facp1  11168  facnn2  11172  faclbnd3  11181  bcn1  11196  hashfz0  11266  hashfibc  11283  hashf1lem2  11286  wrdf  11310  swrdswrdlem  11476  swrdswrd  11477  swrdccatin1  11497  pfxccatin12lem2a  11499  pfxccatin12lem1  11500  swrdccatin2  11501  pfxccatin12lem2  11503  pfxccatin12lem3  11504  pfxccatin12  11505  pfxccat3  11506  swrdccat  11507  swrdccat3blem  11511  cvg1nlemres  11751  rexanuz  11754  fclim  12060  climmo  12064  iser3shft  12112  fsumsplitsn  12177  fsum2dlemstep  12201  fisumcom2  12205  arisum  12265  arisum2  12266  prodmodc  12345  fprodfac  12382  fprod2dlemstep  12389  fprodcom2fi  12393  fprodsplitsn  12400  eftlub  12457  ef01bndlem  12523  sin01gt0  12529  cos01gt0  12530  sin02gt0  12531  dvdsdivcl  12617  addmodlteqALT  12626  odd2np1  12640  oddge22np1  12648  m1expe  12666  nn0enne  12669  nn0o1gt2  12672  nno  12673  ndvdsadd  12698  dfgcd2  12791  mulgcd  12793  algfx  12830  prmind2  12898  prm2orodd  12904  prmgt1  12910  oddprmgt2  12912  dfphi2  12998  nnnn0modprm0  13034  prm23lt5  13042  pythagtriplem2  13045  pcz  13111  dvdsprmpweqnn  13115  oddprmdvds  13133  prmunb  13141  4sqlem4  13171  4sqlem19  13188  ballotfilem2  13228  ballotfilem7  13279  evenennn  13284  fngzsum  13708  gzsumvalx  13709  dfgrp3me  13905  mulgnn0gzsum  13931  rngdi  14239  rngdir  14240  dvdsrcl2  14406  unitinvcl  14430  unitinvinv  14431  unitlinv  14433  unitrinv  14434  opprdrng  14620  rmodislmodlem  14687  rmodislmod  14688  zrhval  14952  psrbagf  15054  distop  15186  ntrss  15220  ssntr  15223  lmrcl  15293  txuni2  15357  txcn  15376  hmeocnvb  15419  xmetunirn  15459  blssioo  15654  divcnap  15666  cdivcncfap  15705  dedekindeulemlub  15721  dedekindicclemlub  15730  dvexp2  15813  elply2  15836  plyco  15860  pilem3  15884  sincosq1sgn  15927  sincosq2sgn  15928  sincosq3sgn  15929  sincosq4sgn  15930  sinq12gt0  15931  logfac  15995  birthdaylem1g  16087  fsumdvdsmul  16105  zabsle1  16118  lgsdir2lem4  16150  gausslemma2dlem0f  16173  gausslemma2dlem1a  16177  gausslemma2dlem2  16181  gausslemma2dlem3  16182  gausslemma2dlem4  16183  2lgslem1a1  16205  2lgslem3  16220  2lgsoddprmlem3  16230  2lgsoddprm  16232  2sqlem2  16234  2sqlem10  16244  vtxvalprc  16296  iedgvalprc  16297  upgrex  16344  umgredg  16386  ausgrusgrben  16409  usgruspgrben  16427  usgrislfuspgrdom  16431  uhgr2edg  16447  uspgredg2v  16462  griedg0ssusgr  16492  subusgr  16516  wlkv  16567  wlk1walkdom  16600  trlsv  16625  trlf1  16629  clwwlk1loop  16640  clwwlkext2edg  16663  umgr2cwwkdifex  16666  clwwlknonex2lem2  16679  clwwlknonex2e  16681  eupthv  16687  eupth2lem3lem4fi  16714  konigsberglem5  16733  bj-pm2.18st  16778  bj-dcstab  16784  decidi  16823  sumdc2  16827  bj-charfunbi  16837  bdel  16871  bdssex  16928  bj-indind  16958  findset  16971  wexmiddc  17042  wexmiddifxy  17046  nninfall  17052  trirec0  17093  neap0mkv  17119  alsex  17139  ralsex  17140