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  714  dcim  841  dcstab  844  stdcndc  845  stdcndcOLD  846  dcor  935  3mix1  1166  3mix2  1167  3jca  1177  syl3anbrc  1181  syl21anbrc  1182  inegd  1372  pclem6  1374  xoranor  1377  nfxfrd  1475  nfd  1523  hban  1547  nfan1  1564  nford  1567  nfand  1568  hbim1  1570  nfal  1576  alexim  1645  nnal  1649  ax6blem  1650  nf4r  1671  19.34  1684  nfexd  1761  sbcof2  1810  nfsb2or  1837  sbidm  1851  nfdv  1877  nfd2  2022  nfeudv  2041  mon  2055  eumo  2058  mo23  2067  eu2  2070  eu3h  2071  exmodc  2076  exmonim  2077  mo2r  2078  mo3h  2079  bm1.1  2162  eqrdv  2175  3eltr4g  2263  abbi2dv  2296  abbi1dv  2297  nfcd  2314  nfcxfrd  2317  dcned  2353  neqned  2354  3netr4g  2382  necon3bi  2397  necon2ai  2401  nnral  2467  alral  2522  rspe  2526  rsp2e  2528  rgen2a  2531  ralrimi  2548  r19.27v  2604  r19.28v  2605  r19.27av  2612  r19.32r  2623  nfreudxy  2651  mormo  2689  nrexrmo  2694  cgsex2g  2775  cgsex4g  2776  spc2egv  2829  spc2gv  2830  spc3egv  2831  spc3gv  2832  rspce  2838  ceqex  2866  elrab3t  2894  elrabd  2897  mosubt  2916  mo2icl  2918  reu3  2929  reu6i  2930  2rmorex  2945  sbc5  2988  rspesbca  3049  rmo2ilem  3054  sbnfc2  3119  ssrd  3162  ssrdv  3163  3sstr4g  3200  eqsstrid  3203  ss2abdv  3230  abssdv  3231  rabssdv  3237  ss2rabdv  3238  ssun1  3300  unssad  3314  unssbd  3315  ssddif  3371  uneqin  3388  indifdir  3393  undif3ss  3398  reuss2  3417  n0rf  3437  reximdva0m  3440  rabxmdc  3456  ssindif0im  3484  minel  3486  ralidm  3525  ralm  3529  dcun  3535  ifmdc  3576  disjsn2  3657  absneu  3666  rabsneu  3667  opprc  3801  elunii  3816  dfnfc2  3829  uniss2  3842  unidif  3843  ssunieq  3844  intab  3875  iunss2  3933  iunssd  3934  iunxdif2  3937  invdisj  3999  disjiun  4000  3brtr4g  4039  trin  4113  triun  4116  truni  4117  trint  4118  iinexgm  4156  class2seteq  4165  pwuni  4194  exmid1dc  4202  exmidn0m  4203  exmidsssn  4204  exmid0el  4206  exmidel  4207  exmidundif  4208  exmidundifim  4209  exmid1stab  4210  mss  4228  copsex2t  4247  euotd  4256  pwunim  4288  ispod  4306  sotricim  4325  exse  4338  frind  4354  trssord  4382  suctr  4423  pwnex  4451  eusvnf  4455  eusvnfb  4456  eusv2nf  4458  rexxfrd  4465  ralxfr2d  4466  rexxfr2d  4467  rabxfrd  4471  reuhypd  4473  eldifpw  4479  iunpw  4482  ssorduni  4488  onsucb  4504  onsucelsucr  4509  sucunielr  4511  ontriexmidim  4523  ordtri2or2exmidlem  4527  onsucelsucexmid  4531  reg2exmidlema  4535  setindel  4539  elirr  4542  orddisj  4547  en2lp  4555  suc11g  4558  ordsuc  4564  nlimsucg  4567  ordtri2or2exmid  4572  ontri2orexmidim  4573  zfregfr  4575  wessep  4579  tfi  4583  peano5  4599  limom  4615  peano2b  4616  nndceq0  4619  nnpredcl  4624  0nelrel  4674  eqrelrdv  4724  xpsspw  4740  relint  4752  relop  4779  eqbrrdva  4799  opeldm  4832  elres  4945  relssres  4947  elrelimasn  4996  exse2  5004  issref  5013  trin2  5022  dminss  5045  imainss  5046  rnxpid  5065  dmsn0el  5100  dmmptg  5128  relrelss  5157  cnviinm  5172  iotanul  5195  sniota  5209  dffun5r  5230  funmo  5233  funco  5258  funun  5262  funprg  5268  funtpg  5269  funtp  5271  fntpg  5274  fununi  5286  funcnvuni  5287  imadiflem  5297  imainlem  5299  funimaexglem  5301  isarep2  5305  fnunsn  5325  2elresin  5329  fnimadisj  5338  dmmptd  5348  fco  5383  funssxp  5387  fssres  5393  feu  5400  fimacnvdisj  5402  fabexg  5405  f00  5409  f0rn0  5412  f1co  5435  fores  5449  foco  5450  f1ores  5478  foimacnv  5481  f1oun  5483  fun11iun  5484  f1oco  5486  fo00  5499  brprcneu  5510  fv3  5540  relelfvdm  5549  nfvres  5550  nfunsn  5551  funfvbrb  5632  respreima  5647  dff2  5663  dff3im  5664  dffo4  5667  fvmptelcdm  5672  ffvresb  5682  f1oresrab  5684  fmptco  5685  fsn  5691  fpr  5701  ftpg  5703  fsnunf  5719  fsnunfv  5720  elabrex  5761  dff1o6  5780  foeqcnvco  5794  fliftel1  5798  isores1  5818  isoini2  5823  riotasbc  5849  acexmidlemph  5871  acexmidlemcase  5873  oprabidlem  5909  brabvv  5924  eloprabga  5965  fnoprabg  5979  caovimo  6071  oprabexd  6131  fo1stresm  6165  fo2ndresm  6166  unielxp  6178  1st2ndbr  6188  fmpoco  6220  1stconst  6225  2ndconst  6226  poxp  6236  spc2ed  6237  disjxp1  6240  reldmtpos  6257  tposfun  6264  dftpos4  6267  smores  6296  smores2  6298  tfrlem1  6312  tfr0dm  6326  tfrlemibxssdm  6331  tfrlemibex  6333  tfrlemiubacc  6334  tfrlemi14d  6337  tfrexlem  6338  tfri1d  6339  tfr1onlembxssdm  6347  tfr1onlembex  6349  tfr1onlemubacc  6350  tfr1onlemres  6353  tfrcllemsucfn  6357  tfrcllembxssdm  6360  tfrcllembex  6362  tfrcllemubacc  6363  tfrcllemres  6366  tfri3  6371  rdgon  6390  frecabcl  6403  frecfcllem  6408  frecrdg  6412  2oconcl  6443  nnsucelsuc  6495  nntri3or  6497  nndceq  6503  nndcel  6504  dcdifsnid  6508  ecexr  6543  brdifun  6565  ecelqsdm  6608  iinerm  6610  eroveu  6629  erovlem  6630  ecopovtrn  6635  ecopovtrng  6638  th3qlem1  6640  pmsspw  6686  map0b  6690  mapsn  6693  mapsncnv  6698  ixpf  6723  uniixp  6724  ixpexgg  6725  resixp  6736  f1oen3g  6757  ssdomg  6781  domtr  6788  snfig  6817  enpr2d  6820  xpf1o  6847  xpmapenlem  6852  php5dom  6866  fidceq  6872  nnfi  6875  fiunsnnn  6884  findcard  6891  findcard2  6892  findcard2s  6893  ac6sfi  6901  tridc  6902  fimax2gtri  6904  finexdc  6905  exmidpw  6911  exmidpweq  6912  nnwetri  6918  unsnfi  6921  unsnfidcex  6922  unsnfidcel  6923  undifdcss  6925  tpfidisj  6930  iunfidisj  6948  snexxph  6952  fidcenumlemrks  6955  sbthlem2  6960  sbthlemi3  6961  sbthlem7  6965  sbthlemi8  6966  fival  6972  dcfi  6983  supmoti  6995  djuss  7072  updjudhf  7081  updjud  7084  casefun  7087  caseinj  7091  omp1eomlem  7096  djufun  7106  djuinj  7108  ctssdccl  7113  ctfoex  7120  nnnninf  7127  nnnninfeq2  7130  nninfisollem0  7131  nninfisollemne  7132  nninfisollemeq  7133  nninfisol  7134  finomni  7141  exmidomniim  7142  exmidomni  7143  fodjuomnilemdc  7145  omniwomnimkv  7168  nninfdcinf  7172  nninfwlporlem  7174  nninfwlpoimlemg  7176  nninfwlpoim  7179  exmidonfinlem  7195  exmidfodomrlemr  7204  exmidfodomrlemrALT  7205  exmidaclem  7210  dju1en  7215  exmidontriimlem1  7223  exmidontriimlem3  7225  pw1on  7228  3nsssucpw1  7238  2omotaplemap  7259  2omotap  7261  exmidmotap  7263  cc4f  7271  cc4n  7273  dmaddpqlem  7379  nqpi  7380  dmaddpq  7381  dmmulpq  7382  ltdcnq  7399  subhalfnqq  7416  enq0sym  7434  enq0ref  7435  enq0tr  7436  nqnq0pi  7440  nq0nn  7444  addnq0mo  7449  mulnq0mo  7450  nqpnq0nq  7455  nqnq0a  7456  nqnq0m  7457  npsspw  7473  elnp1st2nd  7478  prnmaxl  7490  prnminu  7491  prarloc  7505  genprndl  7523  genprndu  7524  nqprm  7544  nqprl  7553  nqpru  7554  addnqprlemrl  7559  addnqprlemru  7560  prmuloc  7568  mulnqprlemrl  7575  mulnqprlemru  7576  ltsopr  7598  ltexprlemm  7602  ltexprlemopl  7603  ltexprlemopu  7605  lteupri  7619  recexprlemopl  7627  recexprlemopu  7629  recexprlemdisj  7632  archpr  7645  cauappcvgprlemdisj  7653  cauappcvgprlemladdrl  7659  cauappcvgprlem2  7662  caucvgprlemnbj  7669  caucvgprlemdisj  7676  caucvgprlemladdfu  7679  caucvgprlem2  7682  caucvgprprlemnbj  7695  caucvgprprlemdisj  7704  suplocexprlemml  7718  suplocexprlemrl  7719  suplocexprlemmu  7720  suplocexprlemloc  7723  addsrmo  7745  mulsrmo  7746  recexgt0sr  7775  prsrpos  7787  caucvgsrlemasr  7792  suplocsrlemb  7808  suplocsrlempr  7809  suplocsr  7811  elrealeu  7831  pitonn  7850  pitoregt0  7851  pitore  7852  recnnre  7853  axaddcl  7866  axaddrcl  7867  axmulcl  7868  axmulrcl  7869  axrnegex  7881  axcnre  7883  axpre-lttrn  7886  rereceu  7891  axarch  7893  axpre-suploclemres  7903  axpre-suploc  7904  ltxrlt  8026  apirr  8565  divmulasscomap  8656  rerecclap  8690  lbreu  8905  arch  9176  0mnnnnn0  9211  nnm1nn0  9220  elnnnn0c  9224  elnnz1  9279  ztri3or0  9298  nzadd  9308  nn0n0n1ge2  9326  zdceq  9331  zdcle  9332  zdclt  9333  uzind  9367  eluzge3nn  9575  supinfneg  9598  infsupneg  9599  eluz2b2  9606  elnn1uz2  9610  elnn0dc  9614  elnndc  9615  nn01to3  9620  znq  9627  qaddcl  9638  qmulcl  9640  qreccl  9645  irradd  9649  irrmul  9650  elpq  9651  cnref1o  9653  xnn0dcle  9805  xrpnfdc  9845  xrmnfdc  9846  xaddcom  9864  xnegdi  9871  xpncan  9874  xleadd1a  9876  iooidg  9912  elioo4g  9937  elfzd  10019  fzdcel  10043  fznlem  10044  fzpreddisj  10074  fz0to4untppr  10127  elfz0ubfz0  10128  elfz0fzfz0  10129  fz0fzelfz0  10130  fz0fzdiffz0  10133  elfzmlbp  10135  difelfzle  10137  4fvwrd4  10143  fzosplit  10180  elfzo0  10185  fzo1fzo0n0  10186  elfzonn0  10189  fzofzim  10191  elfzo1  10193  elfzom1elp1fzo  10205  fzossfzop1  10215  ssfzo12bi  10228  exfzdc  10243  qdceq  10250  exbtwnzlemstep  10251  exbtwnzlemex  10253  exbtwnz  10254  rebtwn2zlemstep  10256  rebtwn2z  10258  qbtwnxr  10261  modfzo0difsn  10398  frec2uzrand  10408  frec2uzf1od  10409  frecuzrdgrcl  10413  frecuzrdgtcl  10415  frecuzrdgrclt  10418  frecuzrdgfunlem  10422  frecfzennn  10429  seq3f1olemp  10505  seq3f1oleml  10506  ser0f  10518  expcl2lemap  10535  hashunsng  10790  shftfvalg  10830  shftfval  10833  caucvgre  10993  rexanuz  11000  recvguniq  11007  rennim  11014  resqrexlemf  11019  rsqrmo  11039  fimaxre2  11238  climeu  11307  sumdc  11369  summodc  11394  zsumdc  11395  isum  11396  fisumss  11403  isumss2  11404  fsumsplit  11418  sumsnf  11420  fsumsplitsn  11421  sumtp  11425  sumsplitdc  11443  fsum2dlemstep  11445  fisum0diag2  11458  fsumconst  11465  modfsummodlemstep  11468  fsum00  11473  fsumabs  11476  fsumiun  11488  isumlessdc  11507  expcnv  11515  prodmodc  11589  zproddc  11590  iprodap  11591  iprodap0  11593  fprodssdc  11601  prodsnf  11603  fprodsplitdc  11607  fprodsplit  11608  fprodm1  11609  fprod1p  11610  fprodunsn  11615  fprod2dlemstep  11633  fprodsplitsn  11644  ef0lem  11671  modmulconst  11833  dvdsdivcl  11859  dvdsssfz1  11861  dvdsfac  11869  zeoxor  11877  nn0ehalf  11911  nn0oddm1d2  11917  nnoddm1d2  11918  divalglemeunn  11929  divalglemeuneg  11931  zsupcllemstep  11949  infssuzex  11953  gcdsupex  11961  gcdsupcl  11962  bezoutlemnewy  12000  bezoutlemmain  12002  bezoutlemeu  12011  dfgcd2  12018  nnwosdc  12043  algrf  12048  algcvgblem  12052  lcmgcdlem  12080  lcmdvds  12082  coprmgcdb  12091  mulgcddvds  12097  qredeu  12100  cncongr1  12106  cncongr2  12107  isprm2lem  12119  dvdsnprmd  12128  prmdc  12133  oddprmge3  12138  pw2dvdseu  12171  phibndlem  12219  dfphi2  12223  hashdvds  12224  phiprmpw  12225  eulerthlemh  12234  hashgcdeq  12242  phisum  12243  odzdvds  12248  reumodprminv  12256  nnnn0modprm0  12258  prm23ge5  12267  pclemdc  12291  pcdvdsb  12322  difsqpwdvds  12340  oddprmdvds  12355  1arith  12368  4sqlem3  12391  ennnfonelemdc  12403  ennnfonelemh  12408  ennnfonelemhf1o  12417  ennnfonelemf1  12422  ennnfonelemrn  12423  ennnfonelemdm  12424  exmidunben  12430  ctinfomlemom  12431  ctinfom  12432  ctiunctlemudc  12441  ctiunctlemf  12442  ctiunctal  12445  nninfdclemcl  12452  nninfdclemf  12453  nninfdclemp1  12454  isstructim  12479  setsresg  12503  strleund  12565  1strbas  12579  2strbasg  12581  2stropg  12582  restsspw  12704  tgval  12717  ptex  12719  imasaddfnlemg  12741  fnpr2o  12764  fnpr2ob  12765  mgmidsssn0  12809  isnsgrp  12818  sgrpidmndm  12827  mndinvmod  12852  mnd1  12853  mhmeql  12882  grpinveu  12917  mulgval  12992  subgintm  13064  trivsubgsnd  13067  eqgfval  13087  iscmnd  13107  srgfcl  13162  reldvdsrsrg  13267  subrgdvds  13362  lssuni  13456  lssintclm  13477  lspf  13482  istopon  13653  toponcom  13667  topgele  13669  topontopn  13677  tsettps  13678  eltg2b  13694  unitg  13702  tgss2  13719  bastop2  13724  distop  13725  epttop  13730  cldss2  13746  neisspw  13788  neipsm  13794  neiuni  13801  tgcn  13848  tgcnp  13849  cnntr  13865  lmff  13889  txuni2  13896  txbasex  13897  txbas  13898  txcnp  13911  txcnmpt  13913  txcn  13915  txdis  13917  txdis1cn  13918  cnmpt11  13923  cnmpt12  13927  cnmpt21  13931  cnmpt2t  13933  cnmpt22  13934  blsscls2  14133  xmetxpbl  14148  xmettxlem  14149  tgqioo  14187  fsumcncntop  14196  cncfmpt1f  14224  mulcncflem  14230  mulcncf  14231  dedekindeu  14241  dedekindicclemicc  14250  dedekindicc  14251  ivthinclemdisj  14258  limcimo  14274  cnmptlimc  14283  reldvg  14288  dvfvalap  14290  dvfgg  14297  dveflem  14327  dvef  14328  sincn  14330  coscn  14331  reeff1o  14334  pilem3  14344  ioocosf1o  14415  lgsne0  14579  lgseisenlem2  14591  2sqlem2  14602  mul2sq  14603  2sqlem3  14604  2sqlem7  14608  bj-trst  14631  bj-fast  14633  bj-stand  14640  bj-trdc  14644  bj-fadc  14646  decidr  14688  djulclALT  14693  djurclALT  14694  bj-charfunr  14702  bj-indind  14824  bj-2inf  14830  bj-nntrans2  14844  bj-peano4  14847  bj-nnord  14850  bj-inf2vn  14866  bj-inf2vn2  14867  bj-findis  14871  pwf1oexmid  14890  subctctexmid  14891  nnsf  14895  nninfsellemdc  14900  nninffeq  14910  exmidsbthrlem  14911  sbthom  14915  triap  14918  trilpo  14932  apdifflemr  14936  redcwlpo  14944  tridceq  14945  nconstwlpolem0  14952  nconstwlpolem  14954  nconstwlpo  14955  neapmkv  14957  ltlenmkv  14959