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  715  dcim  842  dcstab  845  stdcndc  846  stdcndcOLD  847  dcand  934  dcor  937  3mix1  1168  3mix2  1169  3jca  1179  syl3anbrc  1183  syl21anbrc  1184  inegd  1383  pclem6  1385  xoranor  1388  dcfrompeirce  1460  nfxfrd  1489  nfd  1537  hban  1561  nfan1  1578  nford  1581  nfand  1582  hbim1  1584  nfal  1590  alexim  1659  nnal  1663  ax6blem  1664  nf4r  1685  19.34  1698  nfexd  1775  sbcof2  1824  nfsb2or  1851  sbidm  1865  nfdv  1891  nfd2  2041  nfeudv  2060  mon  2074  eumo  2077  mo23  2086  eu2  2089  eu3h  2090  exmodc  2095  exmonim  2096  mo2r  2097  mo3h  2098  bm1.1  2181  eqrdv  2194  3eltr4g  2282  abbi2dv  2315  abbi1dv  2316  nfcd  2334  nfcxfrd  2337  dcned  2373  neqned  2374  3netr4g  2402  necon3bi  2417  necon2ai  2421  nnral  2487  alral  2542  rspe  2546  rsp2e  2548  rgen2a  2551  ralrimi  2568  r19.27v  2624  r19.28v  2625  r19.27av  2632  r19.32r  2643  nfreudxy  2671  mormo  2713  nrexrmo  2718  cgsex2g  2799  cgsex4g  2800  spc2egv  2854  spc2gv  2855  spc3egv  2856  spc3gv  2857  rspce  2863  ceqex  2891  elrab3t  2919  elrabd  2922  mosubt  2941  mo2icl  2943  reu3  2954  reu6i  2955  2rmorex  2970  sbc5  3013  rspesbca  3074  rmo2ilem  3079  sbnfc2  3145  ssrd  3189  ssrdv  3190  3sstr4g  3227  eqsstrid  3230  ss2abdv  3257  abssdv  3258  rabssdv  3264  ss2rabdv  3265  ssun1  3327  unssad  3341  unssbd  3342  ssddif  3398  uneqin  3415  indifdir  3420  undif3ss  3425  reuss2  3444  n0rf  3464  reximdva0m  3467  rabxmdc  3483  ssindif0im  3511  minel  3513  ralidm  3552  ralm  3555  dcun  3561  ifmdc  3602  disjsn2  3686  absneu  3695  rabsneu  3696  opprc  3830  elunii  3845  dfnfc2  3858  uniss2  3871  unidif  3872  ssunieq  3873  intab  3904  iunss2  3962  iunssd  3963  iunxdif2  3966  invdisj  4028  disjiun  4029  3brtr4g  4068  trin  4142  triun  4145  truni  4146  trint  4147  iinexgm  4188  class2seteq  4197  pwuni  4226  exmid1dc  4234  exmidn0m  4235  exmidsssn  4236  exmid0el  4238  exmidel  4239  exmidundif  4240  exmidundifim  4241  exmid1stab  4242  mss  4260  copsex2t  4279  euotd  4288  pwunim  4322  ispod  4340  sotricim  4359  exse  4372  frind  4388  trssord  4416  suctr  4457  pwnex  4485  eusvnf  4489  eusvnfb  4490  eusv2nf  4492  rexxfrd  4499  ralxfr2d  4500  rexxfr2d  4501  rabxfrd  4505  reuhypd  4507  eldifpw  4513  iunpw  4516  ssorduni  4524  onsucb  4540  onsucelsucr  4545  sucunielr  4547  ontriexmidim  4559  ordtri2or2exmidlem  4563  onsucelsucexmid  4567  reg2exmidlema  4571  setindel  4575  elirr  4578  orddisj  4583  en2lp  4591  suc11g  4594  ordsuc  4600  nlimsucg  4603  ordtri2or2exmid  4608  ontri2orexmidim  4609  zfregfr  4611  wessep  4615  tfi  4619  peano5  4635  limom  4651  peano2b  4652  nndceq0  4655  nnpredcl  4660  0nelrel  4710  eqrelrdv  4760  xpsspw  4776  relint  4788  relop  4817  eqbrrdva  4837  opeldm  4870  elres  4983  relssres  4985  elrelimasn  5036  exse2  5044  issref  5053  trin2  5062  dminss  5085  imainss  5086  rnxpid  5105  dmsn0el  5140  dmmptg  5168  relrelss  5197  cnviinm  5212  iotanul  5235  sniota  5250  dffun5r  5271  funmo  5274  funco  5299  funun  5303  funprg  5309  funtpg  5310  funtp  5312  fntpg  5315  fununi  5327  funcnvuni  5328  imadiflem  5338  imainlem  5340  funimaexglem  5342  isarep2  5346  fnunsn  5368  2elresin  5372  fnimadisj  5381  dmmptd  5391  fco  5426  funssxp  5430  fssres  5436  feu  5443  fimacnvdisj  5445  fabexg  5448  f00  5452  f0rn0  5455  f1co  5478  fores  5493  foco  5494  f1ores  5522  foimacnv  5525  f1oun  5527  fun11iun  5528  f1oco  5530  fo00  5543  brprcneu  5554  fv3  5584  relelfvdm  5593  nfvres  5595  nfunsn  5596  funfvbrb  5678  respreima  5693  dff2  5709  dff3im  5710  dffo4  5713  fvmptelcdm  5718  ffvresb  5728  f1oresrab  5730  fmptco  5731  fsn  5737  fpr  5747  ftpg  5749  fsnunf  5765  fsnunfv  5766  elabrex  5807  dff1o6  5826  foeqcnvco  5840  fliftel1  5844  isores1  5864  isoini2  5869  riotasbc  5896  acexmidlemph  5918  acexmidlemcase  5920  oprabidlem  5956  brabvv  5972  eloprabga  6013  fnoprabg  6027  caovimo  6121  oprabexd  6193  uchoice  6204  fo1stresm  6228  fo2ndresm  6229  unielxp  6241  1st2ndbr  6251  fmpoco  6283  1stconst  6288  2ndconst  6289  poxp  6299  spc2ed  6300  disjxp1  6303  reldmtpos  6320  tposfun  6327  dftpos4  6330  smores  6359  smores2  6361  tfrlem1  6375  tfr0dm  6389  tfrlemibxssdm  6394  tfrlemibex  6396  tfrlemiubacc  6397  tfrlemi14d  6400  tfrexlem  6401  tfri1d  6402  tfr1onlembxssdm  6410  tfr1onlembex  6412  tfr1onlemubacc  6413  tfr1onlemres  6416  tfrcllemsucfn  6420  tfrcllembxssdm  6423  tfrcllembex  6425  tfrcllemubacc  6426  tfrcllemres  6429  tfri3  6434  rdgon  6453  frecabcl  6466  frecfcllem  6471  frecrdg  6475  2oconcl  6506  nnsucelsuc  6558  nntri3or  6560  nndceq  6566  nndcel  6567  dcdifsnid  6571  ecexr  6606  brdifun  6628  ecelqsdm  6673  iinerm  6675  eroveu  6694  erovlem  6695  ecopovtrn  6700  ecopovtrng  6703  th3qlem1  6705  pmsspw  6751  map0b  6755  mapsn  6758  mapsncnv  6763  ixpf  6788  uniixp  6789  ixpexgg  6790  resixp  6801  f1oen3g  6822  ssdomg  6846  domtr  6853  snfig  6882  enpr2d  6885  xpf1o  6914  xpmapenlem  6919  php5dom  6933  fidceq  6939  nnfi  6942  fiunsnnn  6951  findcard  6958  findcard2  6959  findcard2s  6960  ac6sfi  6968  tridc  6969  fimax2gtri  6971  finexdc  6972  exmidpw  6978  exmidpweq  6979  exmidpw2en  6982  nnwetri  6986  unsnfi  6989  unsnfidcex  6990  unsnfidcel  6991  undifdcss  6993  tpfidisj  6999  tpfidceq  7000  iunfidisj  7021  snexxph  7025  fidcenumlemrks  7028  sbthlem2  7033  sbthlemi3  7034  sbthlem7  7038  sbthlemi8  7039  fival  7045  dcfi  7056  supmoti  7068  djuss  7145  updjudhf  7154  updjud  7157  casefun  7160  caseinj  7164  omp1eomlem  7169  djufun  7179  djuinj  7181  ctssdccl  7186  ctfoex  7193  nnnninf  7201  nnnninfeq2  7204  nninfisollem0  7205  nninfisollemne  7206  nninfisollemeq  7207  nninfisol  7208  finomni  7215  exmidomniim  7216  exmidomni  7217  fodjuomnilemdc  7219  omniwomnimkv  7242  nninfdcinf  7246  nninfwlporlem  7248  nninfwlpoimlemg  7250  nninfwlpoim  7254  nninfinfwlpo  7255  exmidonfinlem  7274  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  finacn  7289  exmidaclem  7293  dju1en  7298  exmidontriimlem1  7306  exmidontriimlem3  7308  pw1on  7311  3nsssucpw1  7321  2omotaplemap  7342  2omotap  7344  exmidmotap  7346  cc4f  7354  cc4n  7356  acnccim  7357  dmaddpqlem  7463  nqpi  7464  dmaddpq  7465  dmmulpq  7466  ltdcnq  7483  subhalfnqq  7500  enq0sym  7518  enq0ref  7519  enq0tr  7520  nqnq0pi  7524  nq0nn  7528  addnq0mo  7533  mulnq0mo  7534  nqpnq0nq  7539  nqnq0a  7540  nqnq0m  7541  npsspw  7557  elnp1st2nd  7562  prnmaxl  7574  prnminu  7575  prarloc  7589  genprndl  7607  genprndu  7608  nqprm  7628  nqprl  7637  nqpru  7638  addnqprlemrl  7643  addnqprlemru  7644  prmuloc  7652  mulnqprlemrl  7659  mulnqprlemru  7660  ltsopr  7682  ltexprlemm  7686  ltexprlemopl  7687  ltexprlemopu  7689  lteupri  7703  recexprlemopl  7711  recexprlemopu  7713  recexprlemdisj  7716  archpr  7729  cauappcvgprlemdisj  7737  cauappcvgprlemladdrl  7743  cauappcvgprlem2  7746  caucvgprlemnbj  7753  caucvgprlemdisj  7760  caucvgprlemladdfu  7763  caucvgprlem2  7766  caucvgprprlemnbj  7779  caucvgprprlemdisj  7788  suplocexprlemml  7802  suplocexprlemrl  7803  suplocexprlemmu  7804  suplocexprlemloc  7807  addsrmo  7829  mulsrmo  7830  recexgt0sr  7859  prsrpos  7871  caucvgsrlemasr  7876  suplocsrlemb  7892  suplocsrlempr  7893  suplocsr  7895  elrealeu  7915  pitonn  7934  pitoregt0  7935  pitore  7936  recnnre  7937  axaddcl  7950  axaddrcl  7951  axmulcl  7952  axmulrcl  7953  axrnegex  7965  axcnre  7967  axpre-lttrn  7970  rereceu  7975  axarch  7977  axpre-suploclemres  7987  axpre-suploc  7988  ltxrlt  8111  apirr  8651  divmulasscomap  8742  rerecclap  8776  lbreu  8991  arch  9265  0mnnnnn0  9300  nnm1nn0  9309  elnnnn0c  9313  elnnz1  9368  ztri3or0  9387  nzadd  9397  nn0n0n1ge2  9415  zdceq  9420  zdcle  9421  zdclt  9422  uzind  9456  eluzge3nn  9665  supinfneg  9688  infsupneg  9689  eluz2b2  9696  elnn1uz2  9700  elnn0dc  9704  elnndc  9705  nn01to3  9710  znq  9717  qaddcl  9728  qmulcl  9730  qreccl  9735  irradd  9739  irrmul  9740  elpq  9742  cnref1o  9744  xnn0dcle  9896  xrpnfdc  9936  xrmnfdc  9937  xaddcom  9955  xnegdi  9962  xpncan  9965  xleadd1a  9967  iooidg  10003  elioo4g  10028  elfzd  10110  fzdcel  10134  fznlem  10135  fzpreddisj  10165  fz0to4untppr  10218  elfz0ubfz0  10219  elfz0fzfz0  10220  fz0fzelfz0  10221  fz0fzdiffz0  10224  elfzmlbp  10226  difelfzle  10228  4fvwrd4  10234  fzosplit  10272  elfzo0  10277  fzo1fzo0n0  10278  elfzonn0  10281  fzofzim  10283  elfzo1  10285  elfzom1elp1fzo  10297  fzossfzop1  10307  ssfzo12bi  10320  exfzdc  10335  zsupcllemstep  10338  infssuzex  10342  qdceq  10353  qdclt  10354  exbtwnzlemstep  10356  exbtwnzlemex  10358  exbtwnz  10359  rebtwn2zlemstep  10361  rebtwn2z  10363  qbtwnxr  10366  modfzo0difsn  10506  frec2uzrand  10516  frec2uzf1od  10517  frecuzrdgrcl  10521  frecuzrdgtcl  10523  frecuzrdgrclt  10526  frecuzrdgfunlem  10530  frecfzennn  10537  nninfinf  10554  seq3f1olemp  10626  seq3f1oleml  10627  seqf1oglem1  10630  ser0f  10645  expcl2lemap  10662  hashunsng  10918  iswrdinn0  10959  snopiswrd  10964  wrdlndm  10971  iswrdsymb  10972  wrdsymb1  10990  shftfvalg  11002  shftfval  11005  caucvgre  11165  rexanuz  11172  recvguniq  11179  rennim  11186  resqrexlemf  11191  rsqrmo  11211  fimaxre2  11411  climeu  11480  sumdc  11542  summodc  11567  zsumdc  11568  isum  11569  fisumss  11576  isumss2  11577  fsumsplit  11591  sumsnf  11593  fsumsplitsn  11594  sumtp  11598  sumsplitdc  11616  fsum2dlemstep  11618  fisum0diag2  11631  fsumconst  11638  modfsummodlemstep  11641  fsum00  11646  fsumabs  11649  fsumiun  11661  isumlessdc  11680  expcnv  11688  prodmodc  11762  zproddc  11763  iprodap  11764  iprodap0  11766  fprodssdc  11774  prodsnf  11776  fprodsplitdc  11780  fprodsplit  11781  fprodm1  11782  fprod1p  11783  fprodunsn  11788  fprod2dlemstep  11806  fprodsplitsn  11817  ef0lem  11844  modmulconst  12007  dvdsdivcl  12034  dvdsssfz1  12036  dvdsfac  12044  zeoxor  12053  nn0ehalf  12087  nn0oddm1d2  12093  nnoddm1d2  12094  divalglemeunn  12105  divalglemeuneg  12107  bitsfzolem  12138  bitsinv1  12146  gcdsupex  12151  gcdsupcl  12152  bezoutlemnewy  12190  bezoutlemmain  12192  bezoutlemeu  12201  dfgcd2  12208  nnwosdc  12233  nninfct  12235  algrf  12240  algcvgblem  12244  lcmgcdlem  12272  lcmdvds  12274  coprmgcdb  12283  mulgcddvds  12289  qredeu  12292  cncongr1  12298  cncongr2  12299  isprm2lem  12311  dvdsnprmd  12320  prmdc  12325  oddprmge3  12330  pw2dvdseu  12363  phibndlem  12411  dfphi2  12415  hashdvds  12416  phiprmpw  12417  eulerthlemh  12426  hashgcdeq  12435  phisum  12436  odzdvds  12441  reumodprminv  12449  nnnn0modprm0  12451  prm23ge5  12460  pclemdc  12484  pcdvdsb  12516  difsqpwdvds  12534  oddprmdvds  12550  1arith  12563  4sqlem3  12586  4sqlemafi  12591  4sqlemffi  12592  4sqleminfi  12593  4sqexercise1  12594  4sqlem11  12597  4sqlem19  12605  ennnfonelemdc  12643  ennnfonelemh  12648  ennnfonelemhf1o  12657  ennnfonelemf1  12662  ennnfonelemrn  12663  ennnfonelemdm  12664  exmidunben  12670  ctinfomlemom  12671  ctinfom  12672  ctiunctlemudc  12681  ctiunctlemf  12682  ctiunctal  12685  nninfdclemcl  12692  nninfdclemf  12693  nninfdclemp1  12694  isstructim  12719  setsresg  12743  strleund  12808  1strbas  12822  2strbasg  12824  2stropg  12825  restsspw  12953  tgval  12966  ptex  12968  imasaddfnlemg  13018  fnpr2o  13043  fnpr2ob  13044  mgmidsssn0  13088  fngsum  13092  igsumvalx  13093  isnsgrp  13110  sgrpidmndm  13124  mndinvmod  13149  mnd1  13159  mhmeql  13196  grpinveu  13242  prdsinvlem  13312  mulgval  13330  subgintm  13406  trivsubgsnd  13409  eqgfval  13430  ecqusaddd  13446  ecqusaddcl  13447  ghmeql  13475  iscmnd  13506  imasabl  13544  gsumfzmhm2  13552  rnglz  13579  srgfcl  13607  reldvdsrsrg  13726  rhmopp  13810  subrgdvds  13869  lssuni  13997  lssintclm  14018  lspf  14023  qusmulrng  14166  mulgrhm2  14244  znf1o  14285  psr1clfi  14318  istopon  14335  toponcom  14349  topgele  14351  topontopn  14359  tsettps  14360  eltg2b  14376  unitg  14384  tgss2  14401  bastop2  14406  distop  14407  epttop  14412  cldss2  14428  neisspw  14470  neipsm  14476  neiuni  14483  tgcn  14530  tgcnp  14531  cnntr  14547  lmff  14571  txuni2  14578  txbasex  14579  txbas  14580  txcnp  14593  txcnmpt  14595  txcn  14597  txdis  14599  txdis1cn  14600  cnmpt11  14605  cnmpt12  14609  cnmpt21  14613  cnmpt2t  14615  cnmpt22  14616  blsscls2  14815  xmetxpbl  14830  xmettxlem  14831  tgqioo  14877  fsumcncntop  14889  cncfmpt1f  14920  mulcncflem  14929  mulcncf  14930  dedekindeu  14945  dedekindicclemicc  14954  dedekindicc  14955  ivthinclemdisj  14962  hovercncf  14968  limcimo  14987  cnmptlimc  14996  reldvg  15001  dvfvalap  15003  dvfgg  15010  dvmptfsum  15047  dveflem  15048  dvef  15049  elply2  15057  sincn  15091  coscn  15092  reeff1o  15095  pilem3  15105  ioocosf1o  15176  mpodvdsmulf1o  15312  fsumdvdsmul  15313  perfectlem2  15322  lgsne0  15365  gausslemma2dlem1a  15385  gausslemma2dlem4  15391  lgseisenlem2  15398  lgseisenlem3  15399  lgsquadlem2  15405  2lgslem3  15428  2sqlem2  15442  mul2sq  15443  2sqlem3  15444  2sqlem7  15448  bj-trst  15471  bj-fast  15473  bj-stand  15480  bj-trdc  15484  bj-fadc  15486  decidr  15528  djulclALT  15533  djurclALT  15534  bj-charfunr  15542  bj-indind  15664  bj-2inf  15670  bj-nntrans2  15684  bj-peano4  15687  bj-nnord  15690  bj-inf2vn  15706  bj-inf2vn2  15707  bj-findis  15711  pwf1oexmid  15732  subctctexmid  15733  nnsf  15738  nninfsellemdc  15743  nninffeq  15753  nnnninfen  15754  exmidsbthrlem  15757  sbthom  15761  triap  15764  trilpo  15778  apdifflemr  15782  redcwlpo  15790  tridceq  15791  nconstwlpolem0  15798  nconstwlpolem  15800  nconstwlpo  15801  neapmkv  15803  ltlenmkv  15805