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  oibabs  716  dcim  843  dcstab  846  stdcndc  847  stdcndcOLD  848  dcand  935  dcor  938  3mix1  1169  3mix2  1170  3jca  1180  syl3anbrc  1184  syl21anbrc  1185  inegd  1392  pclem6  1394  xoranor  1397  dcfrompeirce  1470  nfxfrd  1499  nfd  1547  hban  1571  nfan1  1588  nford  1591  nfand  1592  hbim1  1594  nfal  1600  alexim  1669  nnal  1673  ax6blem  1674  nf4r  1695  19.34  1708  nfexd  1785  sbcof2  1834  nfsb2or  1861  sbidm  1875  nfdv  1901  nfd2  2051  nfeudv  2070  mon  2084  eumo  2087  mo23  2096  eu2  2099  eu3h  2100  exmodc  2105  exmonim  2106  mo2r  2107  mo3h  2108  bm1.1  2191  eqrdv  2204  3eltr4g  2292  abbi2dv  2325  abbi1dv  2326  nfcd  2344  nfcxfrd  2347  dcned  2383  neqned  2384  3netr4g  2412  necon3bi  2427  necon2ai  2431  nnral  2497  alral  2552  rspe  2556  rsp2e  2558  rgen2a  2561  ralrimi  2578  r19.27v  2634  r19.28v  2635  r19.27av  2642  r19.32r  2653  nfreudxy  2681  mormo  2723  nrexrmo  2728  cgsex2g  2809  cgsex4g  2810  spc2egv  2864  spc2gv  2865  spc3egv  2866  spc3gv  2867  rspce  2873  ceqex  2901  elrab3t  2929  elrabd  2932  mosubt  2951  mo2icl  2953  reu3  2964  reu6i  2965  2rmorex  2980  sbc5  3023  rspesbca  3084  rmo2ilem  3089  sbnfc2  3155  ssrd  3199  ssrdv  3200  3sstr4g  3237  eqsstrid  3240  ss2abdv  3267  abssdv  3268  rabssdv  3274  ss2rabdv  3275  ssun1  3337  unssad  3351  unssbd  3352  ssddif  3408  uneqin  3425  indifdir  3430  undif3ss  3435  reuss2  3454  n0rf  3474  reximdva0m  3477  rabxmdc  3493  ssindif0im  3521  minel  3523  ralidm  3562  ralm  3565  dcun  3571  ifmdc  3613  disjsn2  3697  absneu  3706  rabsneu  3707  opprc  3842  elunii  3857  dfnfc2  3870  uniss2  3883  unidif  3884  ssunieq  3885  intab  3916  iunss2  3974  iunssd  3975  iunxdif2  3978  invdisj  4040  disjiun  4042  3brtr4g  4081  trin  4156  triun  4159  truni  4160  trint  4161  iinexgm  4202  class2seteq  4211  pwuni  4240  exmid1dc  4248  exmidn0m  4249  exmidsssn  4250  exmid0el  4252  exmidel  4253  exmidundif  4254  exmidundifim  4255  exmid1stab  4256  mss  4274  copsex2t  4293  euotd  4303  pwunim  4337  ispod  4355  sotricim  4374  exse  4387  frind  4403  trssord  4431  suctr  4472  pwnex  4500  eusvnf  4504  eusvnfb  4505  eusv2nf  4507  rexxfrd  4514  ralxfr2d  4515  rexxfr2d  4516  rabxfrd  4520  reuhypd  4522  eldifpw  4528  iunpw  4531  ssorduni  4539  onsucb  4555  onsucelsucr  4560  sucunielr  4562  ontriexmidim  4574  ordtri2or2exmidlem  4578  onsucelsucexmid  4582  reg2exmidlema  4586  setindel  4590  elirr  4593  orddisj  4598  en2lp  4606  suc11g  4609  ordsuc  4615  nlimsucg  4618  ordtri2or2exmid  4623  ontri2orexmidim  4624  zfregfr  4626  wessep  4630  tfi  4634  peano5  4650  limom  4666  peano2b  4667  nndceq0  4670  nnpredcl  4675  0nelrel  4725  eqrelrdv  4775  xpsspw  4791  relint  4803  relop  4832  eqbrrdva  4852  ssrelrn  4874  opeldm  4886  elres  5000  relssres  5002  elrelimasn  5053  exse2  5061  issref  5070  trin2  5079  dminss  5102  imainss  5103  rnxpid  5122  dmsn0el  5157  dmmptg  5185  relrelss  5214  cnviinm  5229  iotanul  5252  sniota  5267  dffun5r  5288  funmo  5291  funco  5316  funun  5320  fununmo  5321  fununfun  5322  funprg  5329  funtpg  5330  funtp  5332  fntpg  5335  fununi  5347  funcnvuni  5348  imadiflem  5358  imainlem  5360  funimaexglem  5362  isarep2  5366  fnunsn  5388  2elresin  5392  fnimadisj  5402  dmmptd  5412  fco  5447  funssxp  5451  fssres  5458  feu  5465  fimacnvdisj  5467  fabexg  5470  f00  5474  f0rn0  5477  f1co  5500  fores  5515  foco  5516  f1ores  5544  foimacnv  5547  f1oun  5549  fun11iun  5550  f1oco  5552  fo00  5565  brprcneu  5576  fv3  5606  relelfvdm  5615  nfvres  5617  nfunsn  5618  funfvbrb  5700  respreima  5715  dff2  5731  dff3im  5732  dffo4  5735  fvmptelcdm  5740  ffvresb  5750  f1oresrab  5752  fmptco  5753  fsn  5759  fpr  5773  ftpg  5775  fsnunf  5791  fsnunfv  5792  elabrex  5833  dff1o6  5852  foeqcnvco  5866  fliftel1  5870  isores1  5890  isoini2  5895  riotasbc  5922  acexmidlemph  5944  acexmidlemcase  5946  oprabidlem  5982  brabvv  5998  eloprabga  6039  fnoprabg  6053  caovimo  6147  oprabexd  6219  uchoice  6230  fo1stresm  6254  fo2ndresm  6255  unielxp  6267  1st2ndbr  6277  fmpoco  6309  1stconst  6314  2ndconst  6315  poxp  6325  spc2ed  6326  disjxp1  6329  reldmtpos  6346  tposfun  6353  dftpos4  6356  smores  6385  smores2  6387  tfrlem1  6401  tfr0dm  6415  tfrlemibxssdm  6420  tfrlemibex  6422  tfrlemiubacc  6423  tfrlemi14d  6426  tfrexlem  6427  tfri1d  6428  tfr1onlembxssdm  6436  tfr1onlembex  6438  tfr1onlemubacc  6439  tfr1onlemres  6442  tfrcllemsucfn  6446  tfrcllembxssdm  6449  tfrcllembex  6451  tfrcllemubacc  6452  tfrcllemres  6455  tfri3  6460  rdgon  6479  frecabcl  6492  frecfcllem  6497  frecrdg  6501  2oconcl  6532  nnsucelsuc  6584  nntri3or  6586  nndceq  6592  nndcel  6593  dcdifsnid  6597  ecexr  6632  brdifun  6654  ecelqsdm  6699  iinerm  6701  eroveu  6720  erovlem  6721  ecopovtrn  6726  ecopovtrng  6729  th3qlem1  6731  pmsspw  6777  map0b  6781  mapsn  6784  mapsncnv  6789  ixpf  6814  uniixp  6815  ixpexgg  6816  resixp  6827  f1oen3g  6852  ssdomg  6877  domtr  6884  snfig  6913  enpr2d  6918  xpf1o  6948  xpmapenlem  6953  php5dom  6967  fidceq  6973  nnfi  6976  fiunsnnn  6985  findcard  6992  findcard2  6993  findcard2s  6994  ac6sfi  7002  tridc  7003  fimax2gtri  7005  finexdc  7006  exmidpw  7012  exmidpweq  7013  exmidpw2en  7016  nnwetri  7020  unsnfi  7023  unsnfidcex  7024  unsnfidcel  7025  undifdcss  7027  tpfidisj  7033  tpfidceq  7034  iunfidisj  7055  snexxph  7059  fidcenumlemrks  7062  sbthlem2  7067  sbthlemi3  7068  sbthlem7  7072  sbthlemi8  7073  fival  7079  dcfi  7090  supmoti  7102  djuss  7179  updjudhf  7188  updjud  7191  casefun  7194  caseinj  7198  omp1eomlem  7203  djufun  7213  djuinj  7215  ctssdccl  7220  ctfoex  7227  nnnninf  7235  nnnninfeq2  7238  nninfisollem0  7239  nninfisollemne  7240  nninfisollemeq  7241  nninfisol  7242  finomni  7249  exmidomniim  7250  exmidomni  7251  fodjuomnilemdc  7253  omniwomnimkv  7276  nninfdcinf  7280  nninfwlporlem  7282  nninfwlpoimlemg  7284  nninfwlpoim  7288  nninfinfwlpo  7289  exmidonfinlem  7308  exmidfodomrlemr  7317  exmidfodomrlemrALT  7318  finacn  7323  exmidaclem  7327  dju1en  7332  exmidontriimlem1  7340  exmidontriimlem3  7342  pw1on  7345  3nsssucpw1  7355  2omotaplemap  7376  2omotap  7378  exmidmotap  7380  cc4f  7388  cc4n  7390  acnccim  7391  dmaddpqlem  7497  nqpi  7498  dmaddpq  7499  dmmulpq  7500  ltdcnq  7517  subhalfnqq  7534  enq0sym  7552  enq0ref  7553  enq0tr  7554  nqnq0pi  7558  nq0nn  7562  addnq0mo  7567  mulnq0mo  7568  nqpnq0nq  7573  nqnq0a  7574  nqnq0m  7575  npsspw  7591  elnp1st2nd  7596  prnmaxl  7608  prnminu  7609  prarloc  7623  genprndl  7641  genprndu  7642  nqprm  7662  nqprl  7671  nqpru  7672  addnqprlemrl  7677  addnqprlemru  7678  prmuloc  7686  mulnqprlemrl  7693  mulnqprlemru  7694  ltsopr  7716  ltexprlemm  7720  ltexprlemopl  7721  ltexprlemopu  7723  lteupri  7737  recexprlemopl  7745  recexprlemopu  7747  recexprlemdisj  7750  archpr  7763  cauappcvgprlemdisj  7771  cauappcvgprlemladdrl  7777  cauappcvgprlem2  7780  caucvgprlemnbj  7787  caucvgprlemdisj  7794  caucvgprlemladdfu  7797  caucvgprlem2  7800  caucvgprprlemnbj  7813  caucvgprprlemdisj  7822  suplocexprlemml  7836  suplocexprlemrl  7837  suplocexprlemmu  7838  suplocexprlemloc  7841  addsrmo  7863  mulsrmo  7864  recexgt0sr  7893  prsrpos  7905  caucvgsrlemasr  7910  suplocsrlemb  7926  suplocsrlempr  7927  suplocsr  7929  elrealeu  7949  pitonn  7968  pitoregt0  7969  pitore  7970  recnnre  7971  axaddcl  7984  axaddrcl  7985  axmulcl  7986  axmulrcl  7987  axrnegex  7999  axcnre  8001  axpre-lttrn  8004  rereceu  8009  axarch  8011  axpre-suploclemres  8021  axpre-suploc  8022  ltxrlt  8145  apirr  8685  divmulasscomap  8776  rerecclap  8810  lbreu  9025  arch  9299  0mnnnnn0  9334  nnm1nn0  9343  elnnnn0c  9347  elnnz1  9402  ztri3or0  9421  nzadd  9432  nn0n0n1ge2  9450  zdceq  9455  zdcle  9456  zdclt  9457  uzind  9491  eluzge3nn  9700  supinfneg  9723  infsupneg  9724  eluz2b2  9731  elnn1uz2  9735  elnn0dc  9739  elnndc  9740  nn01to3  9745  znq  9752  qaddcl  9763  qmulcl  9765  qreccl  9770  irradd  9774  irrmul  9775  elpq  9777  cnref1o  9779  xnn0dcle  9931  xrpnfdc  9971  xrmnfdc  9972  xaddcom  9990  xnegdi  9997  xpncan  10000  xleadd1a  10002  iooidg  10038  elioo4g  10063  elfzd  10145  fzdcel  10169  fznlem  10170  fzpreddisj  10200  fz0to4untppr  10253  elfz0ubfz0  10254  elfz0fzfz0  10255  fz0fzelfz0  10256  fz0fzdiffz0  10259  elfzmlbp  10261  difelfzle  10263  4fvwrd4  10269  fzosplit  10308  elfzo0  10313  fzo1fzo0n0  10314  elfzonn0  10317  fzofzim  10319  elfzo1  10321  elfzom1elp1fzo  10338  fzossfzop1  10348  ssfzo12bi  10361  exfzdc  10376  zsupcllemstep  10379  infssuzex  10383  qdceq  10394  qdclt  10395  exbtwnzlemstep  10397  exbtwnzlemex  10399  exbtwnz  10400  rebtwn2zlemstep  10402  rebtwn2z  10404  qbtwnxr  10407  modfzo0difsn  10547  frec2uzrand  10557  frec2uzf1od  10558  frecuzrdgrcl  10562  frecuzrdgtcl  10564  frecuzrdgrclt  10567  frecuzrdgfunlem  10571  frecfzennn  10578  nninfinf  10595  seq3f1olemp  10667  seq3f1oleml  10668  seqf1oglem1  10671  ser0f  10686  expcl2lemap  10703  hashunsng  10959  iswrdinn0  11006  snopiswrd  11011  wrdlndm  11018  iswrdsymb  11019  wrdsymb1  11037  ccatfv0  11067  ccatval21sw  11069  lswccatn0lsw  11075  eqs1  11090  ccat1st1st  11101  lswccats1fst  11104  fzowrddc  11108  swrdfv0  11115  swrdlen2  11123  swrdfv2  11124  swrdsbslen  11127  swrdspsleq  11128  pfxfv0  11151  pfxtrcfv0  11153  pfxeq  11155  pfx1  11162  swrdswrdlem  11163  shftfvalg  11173  shftfval  11176  caucvgre  11336  rexanuz  11343  recvguniq  11350  rennim  11357  resqrexlemf  11362  rsqrmo  11382  fimaxre2  11582  climeu  11651  sumdc  11713  summodc  11738  zsumdc  11739  isum  11740  fisumss  11747  isumss2  11748  fsumsplit  11762  sumsnf  11764  fsumsplitsn  11765  sumtp  11769  sumsplitdc  11787  fsum2dlemstep  11789  fisum0diag2  11802  fsumconst  11809  modfsummodlemstep  11812  fsum00  11817  fsumabs  11820  fsumiun  11832  isumlessdc  11851  expcnv  11859  prodmodc  11933  zproddc  11934  iprodap  11935  iprodap0  11937  fprodssdc  11945  prodsnf  11947  fprodsplitdc  11951  fprodsplit  11952  fprodm1  11953  fprod1p  11954  fprodunsn  11959  fprod2dlemstep  11977  fprodsplitsn  11988  ef0lem  12015  modmulconst  12178  dvdsdivcl  12205  dvdsssfz1  12207  dvdsfac  12215  zeoxor  12224  nn0ehalf  12258  nn0oddm1d2  12264  nnoddm1d2  12265  divalglemeunn  12276  divalglemeuneg  12278  bitsfzolem  12309  bitsinv1  12317  gcdsupex  12322  gcdsupcl  12323  bezoutlemnewy  12361  bezoutlemmain  12363  bezoutlemeu  12372  dfgcd2  12379  nnwosdc  12404  nninfct  12406  algrf  12411  algcvgblem  12415  lcmgcdlem  12443  lcmdvds  12445  coprmgcdb  12454  mulgcddvds  12460  qredeu  12463  cncongr1  12469  cncongr2  12470  isprm2lem  12482  dvdsnprmd  12491  prmdc  12496  oddprmge3  12501  pw2dvdseu  12534  phibndlem  12582  dfphi2  12586  hashdvds  12587  phiprmpw  12588  eulerthlemh  12597  hashgcdeq  12606  phisum  12607  odzdvds  12612  reumodprminv  12620  nnnn0modprm0  12622  prm23ge5  12631  pclemdc  12655  pcdvdsb  12687  difsqpwdvds  12705  oddprmdvds  12721  1arith  12734  4sqlem3  12757  4sqlemafi  12762  4sqlemffi  12763  4sqleminfi  12764  4sqexercise1  12765  4sqlem11  12768  4sqlem19  12776  ennnfonelemdc  12814  ennnfonelemh  12819  ennnfonelemhf1o  12828  ennnfonelemf1  12833  ennnfonelemrn  12834  ennnfonelemdm  12835  exmidunben  12841  ctinfomlemom  12842  ctinfom  12843  ctiunctlemudc  12852  ctiunctlemf  12853  ctiunctal  12856  nninfdclemcl  12863  nninfdclemf  12864  nninfdclemp1  12865  isstructim  12890  setsresg  12914  strleund  12979  1strbas  12993  2strbasg  12996  2stropg  12997  restsspw  13125  tgval  13138  ptex  13140  imasaddfnlemg  13190  fnpr2o  13215  fnpr2ob  13216  mgmidsssn0  13260  fngsum  13264  igsumvalx  13265  isnsgrp  13282  sgrpidmndm  13296  mndinvmod  13321  mnd1  13331  mhmeql  13368  grpinveu  13414  prdsinvlem  13484  mulgval  13502  subgintm  13578  trivsubgsnd  13581  eqgfval  13602  ecqusaddd  13618  ecqusaddcl  13619  ghmeql  13647  iscmnd  13678  imasabl  13716  gsumfzmhm2  13724  rnglz  13751  srgfcl  13779  reldvdsrsrg  13898  rhmopp  13982  subrgdvds  14041  lssuni  14169  lssintclm  14190  lspf  14195  qusmulrng  14338  mulgrhm2  14416  znf1o  14457  psrbagfi  14479  psr1clfi  14494  mplsubgfilemcl  14505  istopon  14529  toponcom  14543  topgele  14545  topontopn  14553  tsettps  14554  eltg2b  14570  unitg  14578  tgss2  14595  bastop2  14600  distop  14601  epttop  14606  cldss2  14622  neisspw  14664  neipsm  14670  neiuni  14677  tgcn  14724  tgcnp  14725  cnntr  14741  lmff  14765  txuni2  14772  txbasex  14773  txbas  14774  txcnp  14787  txcnmpt  14789  txcn  14791  txdis  14793  txdis1cn  14794  cnmpt11  14799  cnmpt12  14803  cnmpt21  14807  cnmpt2t  14809  cnmpt22  14810  blsscls2  15009  xmetxpbl  15024  xmettxlem  15025  tgqioo  15071  fsumcncntop  15083  cncfmpt1f  15114  mulcncflem  15123  mulcncf  15124  dedekindeu  15139  dedekindicclemicc  15148  dedekindicc  15149  ivthinclemdisj  15156  hovercncf  15162  limcimo  15181  cnmptlimc  15190  reldvg  15195  dvfvalap  15197  dvfgg  15204  dvmptfsum  15241  dveflem  15242  dvef  15243  elply2  15251  sincn  15285  coscn  15286  reeff1o  15289  pilem3  15299  ioocosf1o  15370  mpodvdsmulf1o  15506  fsumdvdsmul  15507  perfectlem2  15516  lgsne0  15559  gausslemma2dlem1a  15579  gausslemma2dlem4  15585  lgseisenlem2  15592  lgseisenlem3  15593  lgsquadlem2  15599  2lgslem3  15622  2sqlem2  15636  mul2sq  15637  2sqlem3  15638  2sqlem7  15642  edgstruct  15704  pw0ss  15723  incistruhgr  15730  bj-trst  15749  bj-fast  15751  bj-stand  15758  bj-trdc  15762  bj-fadc  15764  decidr  15806  djulclALT  15811  djurclALT  15812  bj-charfunr  15820  bj-indind  15942  bj-2inf  15948  bj-nntrans2  15962  bj-peano4  15965  bj-nnord  15968  bj-inf2vn  15984  bj-inf2vn2  15985  bj-findis  15989  pwf1oexmid  16010  subctctexmid  16011  nnsf  16016  nninfsellemdc  16021  nninffeq  16031  nnnninfen  16032  exmidsbthrlem  16035  sbthom  16039  triap  16042  trilpo  16056  apdifflemr  16060  redcwlpo  16068  tridceq  16069  nconstwlpolem0  16076  nconstwlpolem  16078  nconstwlpo  16079  neapmkv  16081  ltlenmkv  16083