Theorem sylibr 134

Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
sylibr.1	⊢ (𝜑 → 𝜓)
sylibr.2	⊢ (𝜒 ↔ 𝜓)

Assertion

Ref	Expression
sylibr	⊢ (𝜑 → 𝜒)

Proof of Theorem sylibr

Step	Hyp	Ref	Expression
1		sylibr.1	. 2 ⊢ (𝜑 → 𝜓)
2		sylibr.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	2	biimpri 133	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  sylbbr  136  pm5.74rd  183  bitri  184  3imtr4i  201  sylanbrc  417  mpnanrd  697  oibabs  719  dcim  846  dcstab  849  stdcndc  850  stdcndcOLD  851  dcand  938  dcor  941  dfifp2dc  987  3mix1  1190  3mix2  1191  3jca  1201  syl3anbrc  1205  syl21anbrc  1206  inegd  1414  pclem6  1416  xoranor  1419  dcfrompeirce  1492  nfxfrd  1521  nfd  1569  hban  1593  nfan1  1610  nford  1613  nfand  1614  hbim1  1616  nfal  1622  alexim  1691  nnal  1695  ax6blem  1696  nf4r  1717  19.34  1730  nfexd  1807  sbcof2  1856  nfsb2or  1883  sbidm  1897  nfdv  1923  nfd2  2073  nfeudv  2092  mon  2106  eumo  2109  mo23  2119  eu2  2122  eu3h  2123  exmodc  2128  exmonim  2129  mo2r  2130  mo3h  2131  bm1.1  2214  eqrdv  2227  3eltr4g  2315  abbi2dv  2348  abbi1dv  2349  nfcd  2367  nfcxfrd  2370  dcned  2406  neqned  2407  3netr4g  2435  necon3bi  2450  necon2ai  2454  nnral  2520  alral  2575  rspe  2579  rsp2e  2581  rgen2a  2584  ralrimi  2601  r19.27v  2658  r19.28v  2659  r19.27av  2666  r19.32r  2677  nfreudxy  2705  mormo  2748  nrexrmo  2753  cgsex2g  2837  cgsex4g  2838  spc2egv  2894  spc2gv  2895  spc3egv  2896  spc3gv  2897  rspce  2903  ceqex  2931  elrab3t  2959  elrabd  2962  mosubt  2981  mo2icl  2983  reu3  2994  reu6i  2995  2rmorex  3010  sbc5  3053  rspesbca  3115  rmo2ilem  3120  sbnfc2  3186  ssrd  3230  ssrdv  3231  3sstr4g  3268  eqsstrid  3271  ss2abdv  3298  abssdv  3299  rabssdv  3305  ss2rabdv  3306  ssun1  3368  unssad  3382  unssbd  3383  ssddif  3439  uneqin  3456  indifdir  3461  undif3ss  3466  reuss2  3485  n0rf  3505  reximdva0m  3508  rabxmdc  3524  ssindif0im  3552  minel  3554  ralidm  3593  ralm  3596  dcun  3602  ifmdc  3646  disjsn2  3730  rabsnif  3736  absneu  3741  rabsneu  3742  opprc  3881  elunii  3896  dfnfc2  3909  uniss2  3922  unidif  3923  ssunieq  3924  intab  3955  iunss2  4013  iunssd  4014  iunxdif2  4017  invdisj  4079  disjiun  4081  3brtr4g  4120  trin  4195  triun  4198  truni  4199  trint  4200  iinexgm  4242  class2seteq  4251  pwuni  4280  exmid1dc  4288  exmidn0m  4289  exmidsssn  4290  exmid0el  4292  exmidel  4293  exmidundif  4294  exmidundifim  4295  exmid1stab  4296  mss  4316  copsex2t  4335  euotd  4345  pwunim  4381  ispod  4399  sotricim  4418  exse  4431  frind  4447  trssord  4475  suctr  4516  pwnex  4544  eusvnf  4548  eusvnfb  4549  eusv2nf  4551  rexxfrd  4558  ralxfr2d  4559  rexxfr2d  4560  rabxfrd  4564  reuhypd  4566  eldifpw  4572  iunpw  4575  ssorduni  4583  onsucb  4599  onsucelsucr  4604  sucunielr  4606  ontriexmidim  4618  ordtri2or2exmidlem  4622  onsucelsucexmid  4626  reg2exmidlema  4630  setindel  4634  elirr  4637  orddisj  4642  en2lp  4650  suc11g  4653  ordsuc  4659  nlimsucg  4662  ordtri2or2exmid  4667  ontri2orexmidim  4668  zfregfr  4670  wessep  4674  tfi  4678  peano5  4694  limom  4710  peano2b  4711  nndceq0  4714  nnpredcl  4719  0nelrel  4770  eqrelrdv  4820  xpsspw  4836  relint  4849  relop  4878  eqbrrdva  4898  ssrelrn  4920  opeldm  4932  reldmm  4948  elres  5047  relssres  5049  elrelimasn  5100  exse2  5108  issref  5117  trin2  5126  dminss  5149  imainss  5150  rnxpid  5169  dmsn0el  5204  dmmptg  5232  relrelss  5261  cnviinm  5276  iotanul  5300  sniota  5315  dffun5r  5336  funmo  5339  funco  5364  funun  5368  fununmo  5369  fununfun  5370  funprg  5377  funtpg  5378  funtp  5380  fntpg  5383  fununi  5395  funcnvuni  5396  imadiflem  5406  imainlem  5408  funimaexglem  5410  isarep2  5414  fnunsn  5436  2elresin  5440  fnimadisj  5450  dmmptd  5460  fco  5497  funssxp  5501  fssres  5509  feu  5516  fimacnvdisj  5518  fabexg  5521  f00  5525  f0rn0  5528  f1co  5551  fores  5566  foco  5567  f1ores  5595  foimacnv  5598  f1oun  5600  fun11iun  5601  f1oco  5603  fo00  5617  brprcneu  5628  fv3  5658  relelfvdm  5667  nfvres  5671  nfunsn  5672  funfvbrb  5756  respreima  5771  dff2  5787  dff3im  5788  dffo4  5791  fvmptelcdm  5796  ffvresb  5806  f1oresrab  5808  fmptco  5809  fsn  5815  fcof  5828  fpr  5831  ftpg  5833  fsnunf  5849  fsnunfv  5850  elabrex  5893  dff1o6  5912  foeqcnvco  5926  fliftel1  5930  isores1  5950  isoini2  5955  riotasbc  5983  acexmidlemph  6006  acexmidlemcase  6008  oprabidlem  6044  brabvv  6062  eloprabga  6103  fnoprabg  6117  caovimo  6211  oprabexd  6284  uchoice  6295  fo1stresm  6319  fo2ndresm  6320  unielxp  6332  1st2ndbr  6342  opabn1stprc  6353  fmpoco  6376  1stconst  6381  2ndconst  6382  poxp  6392  spc2ed  6393  disjxp1  6396  elmpom  6398  reldmtpos  6414  tposfun  6421  dftpos4  6424  smores  6453  smores2  6455  tfrlem1  6469  tfr0dm  6483  tfrlemibxssdm  6488  tfrlemibex  6490  tfrlemiubacc  6491  tfrlemi14d  6494  tfrexlem  6495  tfri1d  6496  tfr1onlembxssdm  6504  tfr1onlembex  6506  tfr1onlemubacc  6507  tfr1onlemres  6510  tfrcllemsucfn  6514  tfrcllembxssdm  6517  tfrcllembex  6519  tfrcllemubacc  6520  tfrcllemres  6523  tfri3  6528  rdgon  6547  frecabcl  6560  frecfcllem  6565  frecrdg  6569  2oconcl  6602  nnsucelsuc  6654  nntri3or  6656  nndceq  6662  nndcel  6663  dcdifsnid  6667  ecexr  6702  brdifun  6724  ecelqsdm  6769  iinerm  6771  eroveu  6790  erovlem  6791  ecopovtrn  6796  ecopovtrng  6799  th3qlem1  6801  pmsspw  6847  map0b  6851  mapsn  6854  mapsncnv  6859  ixpf  6884  uniixp  6885  ixpexgg  6886  resixp  6897  f1oen3g  6922  ssdomg  6947  domtr  6954  snfig  6984  modom  6989  enpr2d  6992  dom1o  6997  xpf1o  7025  xpmapenlem  7030  php5dom  7044  fidceq  7051  nnfi  7054  fiunsnnn  7065  findcard  7072  findcard2  7073  findcard2s  7074  ac6sfi  7082  fidcen  7083  tridc  7084  fimax2gtri  7086  finexdc  7087  elssdc  7089  eqsndc  7090  exmidpw  7095  exmidpweq  7096  exmidpw2en  7099  nnwetri  7103  unsnfi  7106  unsnfidcex  7107  unsnfidcel  7108  undifdcss  7110  tpfidisj  7116  tpfidceq  7117  exmidssfi  7125  iunfidisj  7139  snexxph  7143  fidcenumlemrks  7146  sbthlem2  7151  sbthlemi3  7152  sbthlem7  7156  sbthlemi8  7157  fival  7163  dcfi  7174  supmoti  7186  djuss  7263  updjudhf  7272  updjud  7275  casefun  7278  caseinj  7282  omp1eomlem  7287  djufun  7297  djuinj  7299  ctssdccl  7304  ctfoex  7311  nnnninf  7319  nnnninfeq2  7322  nninfisollem0  7323  nninfisollemne  7324  nninfisollemeq  7325  nninfisol  7326  finomni  7333  exmidomniim  7334  exmidomni  7335  fodjuomnilemdc  7337  omniwomnimkv  7360  nninfdcinf  7364  nninfwlporlem  7366  nninfwlpoimlemg  7368  nninfwlpoim  7372  nninfinfwlpo  7373  exmidonfinlem  7397  exmidfodomrlemr  7406  exmidfodomrlemrALT  7407  finacn  7412  exmidaclem  7416  dju1en  7421  exmidontriimlem1  7429  exmidontriimlem3  7431  iftrueb01  7434  pw1on  7437  3nsssucpw1  7447  2omotaplemap  7469  2omotap  7471  exmidmotap  7473  cc4f  7481  cc4n  7483  acnccim  7484  dmaddpqlem  7590  nqpi  7591  dmaddpq  7592  dmmulpq  7593  ltdcnq  7610  subhalfnqq  7627  enq0sym  7645  enq0ref  7646  enq0tr  7647  nqnq0pi  7651  nq0nn  7655  addnq0mo  7660  mulnq0mo  7661  nqpnq0nq  7666  nqnq0a  7667  nqnq0m  7668  npsspw  7684  elnp1st2nd  7689  prnmaxl  7701  prnminu  7702  prarloc  7716  genprndl  7734  genprndu  7735  nqprm  7755  nqprl  7764  nqpru  7765  addnqprlemrl  7770  addnqprlemru  7771  prmuloc  7779  mulnqprlemrl  7786  mulnqprlemru  7787  ltsopr  7809  ltexprlemm  7813  ltexprlemopl  7814  ltexprlemopu  7816  lteupri  7830  recexprlemopl  7838  recexprlemopu  7840  recexprlemdisj  7843  archpr  7856  cauappcvgprlemdisj  7864  cauappcvgprlemladdrl  7870  cauappcvgprlem2  7873  caucvgprlemnbj  7880  caucvgprlemdisj  7887  caucvgprlemladdfu  7890  caucvgprlem2  7893  caucvgprprlemnbj  7906  caucvgprprlemdisj  7915  suplocexprlemml  7929  suplocexprlemrl  7930  suplocexprlemmu  7931  suplocexprlemloc  7934  addsrmo  7956  mulsrmo  7957  recexgt0sr  7986  prsrpos  7998  caucvgsrlemasr  8003  suplocsrlemb  8019  suplocsrlempr  8020  suplocsr  8022  elrealeu  8042  pitonn  8061  pitoregt0  8062  pitore  8063  recnnre  8064  axaddcl  8077  axaddrcl  8078  axmulcl  8079  axmulrcl  8080  axrnegex  8092  axcnre  8094  axpre-lttrn  8097  rereceu  8102  axarch  8104  axpre-suploclemres  8114  axpre-suploc  8115  ltxrlt  8238  apirr  8778  divmulasscomap  8869  rerecclap  8903  lbreu  9118  arch  9392  0mnnnnn0  9427  nnm1nn0  9436  elnnnn0c  9440  elnnz1  9495  ztri3or0  9514  nzadd  9525  nn0n0n1ge2  9543  zdceq  9548  zdcle  9549  zdclt  9550  uzind  9584  eluzge3nn  9799  supinfneg  9822  infsupneg  9823  eluz2b2  9830  elnn1uz2  9834  elnn0dc  9838  elnndc  9839  nn01to3  9844  znq  9851  qaddcl  9862  qmulcl  9864  qreccl  9869  irradd  9873  irrmul  9874  elpq  9876  cnref1o  9878  xnn0dcle  10030  xrpnfdc  10070  xrmnfdc  10071  xaddcom  10089  xnegdi  10096  xpncan  10099  xleadd1a  10101  iooidg  10137  elioo4g  10162  elfzd  10244  fzdcel  10268  fznlem  10269  fzpreddisj  10299  fz0to4untppr  10352  elfz0ubfz0  10353  elfz0fzfz0  10354  fz0fzelfz0  10355  fz0fzdiffz0  10358  elfzmlbp  10360  difelfzle  10362  4fvwrd4  10368  fzosplit  10407  elfzo0  10414  fzo1fzo0n0  10415  elfzonn0  10418  fzofzim  10420  elfzo1  10423  elfzom1elp1fzo  10440  fzossfzop1  10450  ssfzo12bi  10463  exfzdc  10479  zsupcllemstep  10482  infssuzex  10486  qdceq  10497  qdclt  10498  exbtwnzlemstep  10500  exbtwnzlemex  10502  exbtwnz  10503  rebtwn2zlemstep  10505  rebtwn2z  10507  qbtwnxr  10510  modfzo0difsn  10650  frec2uzrand  10660  frec2uzf1od  10661  frecuzrdgrcl  10665  frecuzrdgtcl  10667  frecuzrdgrclt  10670  frecuzrdgfunlem  10674  frecfzennn  10681  nninfinf  10698  seq3f1olemp  10770  seq3f1oleml  10771  seqf1oglem1  10774  ser0f  10789  expcl2lemap  10806  hashunsng  11064  iswrdinn0  11111  snopiswrd  11116  wrdlndm  11123  iswrdsymb  11124  wrdsymb1  11143  ccatfv0  11173  ccatval21sw  11175  lswccatn0lsw  11181  eqs1  11198  ccat1st1st  11211  lswccats1fst  11214  fzowrddc  11221  swrdfv0  11228  swrdlen2  11236  swrdfv2  11237  swrdsbslen  11240  swrdspsleq  11241  pfxfv0  11266  pfxtrcfv0  11268  pfxeq  11270  pfx1  11277  swrdswrdlem  11278  cats1un  11295  pfxccatin12lem2a  11301  pfxccatin12lem2  11305  pfxccatin12lem3  11306  swrdccat  11309  cats1fvn  11338  cats1fvnd  11339  shftfvalg  11372  shftfval  11375  caucvgre  11535  rexanuz  11542  recvguniq  11549  rennim  11556  resqrexlemf  11561  rsqrmo  11581  fimaxre2  11781  climeu  11850  sumdc  11912  summodc  11937  zsumdc  11938  isum  11939  fisumss  11946  isumss2  11947  fsumsplit  11961  sumsnf  11963  fsumsplitsn  11964  sumtp  11968  sumsplitdc  11986  fsum2dlemstep  11988  fisum0diag2  12001  fsumconst  12008  modfsummodlemstep  12011  fsum00  12016  fsumabs  12019  fsumiun  12031  isumlessdc  12050  expcnv  12058  prodmodc  12132  zproddc  12133  iprodap  12134  iprodap0  12136  fprodssdc  12144  prodsnf  12146  fprodsplitdc  12150  fprodsplit  12151  fprodm1  12152  fprod1p  12153  fprodunsn  12158  fprod2dlemstep  12176  fprodsplitsn  12187  ef0lem  12214  modmulconst  12377  dvdsdivcl  12404  dvdsssfz1  12406  dvdsfac  12414  zeoxor  12423  nn0ehalf  12457  nn0oddm1d2  12463  nnoddm1d2  12464  divalglemeunn  12475  divalglemeuneg  12477  bitsfzolem  12508  bitsinv1  12516  gcdsupex  12521  gcdsupcl  12522  bezoutlemnewy  12560  bezoutlemmain  12562  bezoutlemeu  12571  dfgcd2  12578  nnwosdc  12603  nninfct  12605  algrf  12610  algcvgblem  12614  lcmgcdlem  12642  lcmdvds  12644  coprmgcdb  12653  mulgcddvds  12659  qredeu  12662  cncongr1  12668  cncongr2  12669  isprm2lem  12681  dvdsnprmd  12690  prmdc  12695  oddprmge3  12700  pw2dvdseu  12733  phibndlem  12781  dfphi2  12785  hashdvds  12786  phiprmpw  12787  eulerthlemh  12796  hashgcdeq  12805  phisum  12806  odzdvds  12811  reumodprminv  12819  nnnn0modprm0  12821  prm23ge5  12830  pclemdc  12854  pcdvdsb  12886  difsqpwdvds  12904  oddprmdvds  12920  1arith  12933  4sqlem3  12956  4sqlemafi  12961  4sqlemffi  12962  4sqleminfi  12963  4sqexercise1  12964  4sqlem11  12967  4sqlem19  12975  ennnfonelemdc  13013  ennnfonelemh  13018  ennnfonelemhf1o  13027  ennnfonelemf1  13032  ennnfonelemrn  13033  ennnfonelemdm  13034  exmidunben  13040  ctinfomlemom  13041  ctinfom  13042  ctiunctlemudc  13051  ctiunctlemf  13052  ctiunctal  13055  nninfdclemcl  13062  nninfdclemf  13063  nninfdclemp1  13064  isstructim  13089  setsresg  13113  strleund  13179  1strbas  13193  2strbasg  13196  2stropg  13197  restsspw  13325  tgval  13338  ptex  13340  imasaddfnlemg  13390  fnpr2o  13415  fnpr2ob  13416  mgmidsssn0  13460  fngsum  13464  igsumvalx  13465  isnsgrp  13482  sgrpidmndm  13496  mndinvmod  13521  mnd1  13531  mhmeql  13568  grpinveu  13614  prdsinvlem  13684  mulgval  13702  subgintm  13778  trivsubgsnd  13781  eqgfval  13802  ecqusaddd  13818  ecqusaddcl  13819  ghmeql  13847  iscmnd  13878  imasabl  13916  gsumfzmhm2  13924  rnglz  13951  srgfcl  13979  rhmopp  14183  subrgdvds  14242  lssuni  14370  lssintclm  14391  lspf  14396  qusmulrng  14539  mulgrhm2  14617  znf1o  14658  psrbagfi  14680  psr1clfi  14695  mplsubgfilemcl  14706  istopon  14730  toponcom  14744  topgele  14746  topontopn  14754  tsettps  14755  eltg2b  14771  unitg  14779  tgss2  14796  bastop2  14801  distop  14802  epttop  14807  cldss2  14823  neisspw  14865  neipsm  14871  neiuni  14878  tgcn  14925  tgcnp  14926  cnntr  14942  lmff  14966  txuni2  14973  txbasex  14974  txbas  14975  txcnp  14988  txcnmpt  14990  txcn  14992  txdis  14994  txdis1cn  14995  cnmpt11  15000  cnmpt12  15004  cnmpt21  15008  cnmpt2t  15010  cnmpt22  15011  blsscls2  15210  xmetxpbl  15225  xmettxlem  15226  tgqioo  15272  fsumcncntop  15284  cncfmpt1f  15315  mulcncflem  15324  mulcncf  15325  dedekindeu  15340  dedekindicclemicc  15349  dedekindicc  15350  ivthinclemdisj  15357  hovercncf  15363  limcimo  15382  cnmptlimc  15391  reldvg  15396  dvfvalap  15398  dvfgg  15405  dvmptfsum  15442  dveflem  15443  dvef  15444  elply2  15452  sincn  15486  coscn  15487  reeff1o  15490  pilem3  15500  ioocosf1o  15571  mpodvdsmulf1o  15707  fsumdvdsmul  15708  perfectlem2  15717  lgsne0  15760  gausslemma2dlem1a  15780  gausslemma2dlem4  15786  lgseisenlem2  15793  lgseisenlem3  15794  lgsquadlem2  15800  2lgslem3  15823  2sqlem2  15837  mul2sq  15838  2sqlem3  15839  2sqlem7  15843  edgstruct  15908  pw0ss  15927  incistruhgr  15934  upgrex  15947  umgrnloop0  15961  upgr1een  15968  lfgrnloopen  15977  umgredg  15989  umgrnloop2  15995  uspgredgiedg  16022  uspgriedgedg  16023  usgrislfuspgrdom  16034  usgredg3  16058  uspgredg2vlem  16064  uspgredg2v  16065  ushgredgedg  16070  ushgredgedgloop  16072  uhgr0vsize0en  16079  usgr1e  16085  vtxedgfi  16100  vtxlpfi  16101  vtxdumgrfival  16109  1loopgrvd2fi  16116  p1evtxdeqfilem  16122  vdegp1aid  16125  wlkcprim  16161  wlk1walkdom  16170  uspgr2wlkeq  16176  upgr2wlkdc  16186  wlkres  16188  clwwlkccatlem  16209  clwwlknp  16226  umgr2cwwk2dif  16233  bj-trst  16285  bj-fast  16287  bj-stand  16294  bj-trdc  16298  bj-fadc  16300  decidr  16342  djulclALT  16347  djurclALT  16348  bj-charfunr  16355  bj-indind  16477  bj-2inf  16483  bj-nntrans2  16497  bj-peano4  16500  bj-nnord  16503  bj-inf2vn  16519  bj-inf2vn2  16520  bj-findis  16524  pwf1oexmid  16550  subctctexmid  16551  pw1dceq  16555  nnsf  16557  nninfsellemdc  16562  nninffeq  16572  nnnninfen  16573  exmidsbthrlem  16576  sbthom  16580  triap  16583  trilpo  16597  apdifflemr  16601  redcwlpo  16609  tridceq  16610  nconstwlpolem0  16617  nconstwlpolem  16619  nconstwlpo  16620  neapmkv  16622  ltlenmkv  16624