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  421  mpnanrd  704  oibabs  726  dcim  853  dcstab  856  stdcndc  857  stdcndcOLD  858  dcand  945  dcor  948  dfifp2dc  994  3mix1  1197  3mix2  1198  3jca  1208  syl3anbrc  1212  syl21anbrc  1213  inegd  1421  pclem6  1423  xoranor  1426  dcfrompeirce  1499  nfxfrd  1528  nfd  1576  hban  1600  nfan1  1617  nford  1620  nfand  1621  hbim1  1623  nfal  1629  alexim  1698  nnal  1702  hbn  1703  nf4r  1723  19.34  1736  nfexd  1814  sbcof2  1863  nfsb2or  1890  sbidm  1904  nfdv  1930  nfd2  2082  nfeudv  2101  mon  2115  eumo  2118  mo23  2128  eu2  2131  eu3h  2132  exmodc  2137  exmonim  2138  mo2r  2139  mo3h  2140  bm1.1  2223  eqrdv  2236  3eltr4g  2324  abbi2dv  2359  abbi1dv  2360  nfcd  2387  nfcxfrd  2390  dcned  2426  neqned  2427  3netr4g  2455  necon3bi  2470  necon2ai  2474  nnral  2540  alral  2595  rspe  2599  rsp2e  2601  rgen2a  2604  ralrimi  2621  r19.27v  2678  r19.28v  2679  r19.27av  2686  r19.32r  2697  nfreudxy  2725  mormo  2769  nrexrmo  2774  cgsex2g  2858  cgsex4g  2859  spc2egv  2915  spc2gv  2916  spc3egv  2917  spc3gv  2918  rspce  2924  ceqex  2953  elrab3t  2981  elrabd  2984  mosubt  3003  mo2icl  3005  reu3  3016  reu6i  3017  2rmorex  3032  sbc5  3075  rspesbca  3137  rmo2ilem  3142  sbnfc2  3208  ssrd  3253  ssrdv  3254  3sstr4g  3291  eqsstrid  3294  ss2abdv  3321  abssdv  3322  rabssdv  3328  ss2rabdv  3329  ssun1  3392  unssad  3406  unssbd  3407  ssddif  3465  uneqin  3482  indifdir  3487  undif3ss  3492  reuss2  3513  n0rf  3534  reximdva0m  3537  rabxmdc  3554  ssindif0im  3584  minel  3586  ralidm  3628  ralm  3631  dcun  3637  ifmdc  3683  ifeqeqxdc  3687  disjsn2  3771  rabsnif  3777  absneu  3782  rabsneu  3783  opprc  3923  elunii  3938  dfnfc2  3951  uniss2  3964  unidif  3965  ssunieq  3966  intab  3997  iunss2  4055  iunssd  4056  iunxdif2  4059  invdisj  4121  disjiun  4123  3brtr4g  4162  trin  4237  triun  4240  truni  4241  trint  4242  iinexgm  4288  class2seteq  4298  pwuni  4327  exmid1dc  4335  exmidn0m  4336  exmidsssn  4337  exmid0el  4339  exmidel  4340  exmidundif  4341  exmidundifim  4342  exmid1stab  4343  mss  4364  copsex2t  4383  euotd  4393  pwunim  4429  ispod  4447  sotricim  4466  exse  4479  frind  4495  trssord  4523  suctr  4564  pwnex  4593  eusvnf  4597  eusvnfb  4598  eusv2nf  4600  rexxfrd  4607  ralxfr2d  4608  rexxfr2d  4609  rabxfrd  4613  reuhypd  4615  eldifpw  4621  iunpw  4624  ssorduni  4632  onsucb  4648  onsucelsucr  4653  sucunielr  4655  ontriexmidim  4667  ordtri2or2exmidlem  4671  onsucelsucexmid  4675  reg2exmidlema  4679  setindel  4683  elirr  4686  orddisj  4691  en2lp  4699  suc11g  4702  ordsuc  4708  nlimsucg  4711  ordtri2or2exmid  4716  ontri2orexmidim  4717  zfregfr  4719  wessep  4723  tfi  4727  peano5  4743  limom  4759  peano2b  4760  nndceq0  4763  nnpredcl  4768  0nelrel  4819  eqrelrdv  4869  xpsspw  4885  relint  4899  relop  4928  eqbrrdva  4948  ssrelrn  4970  opeldm  4982  reldmm  4998  elres  5097  relssres  5099  elrelimasn  5151  exse2  5159  issref  5168  trin2  5177  dminss  5200  imainss  5201  rnxpid  5220  dmsn0el  5255  dmmptg  5283  relrelss  5312  cnviinm  5327  iotanul  5351  sniota  5366  dffun5r  5387  funmo  5390  funco  5415  funun  5420  fununmo  5421  fununfun  5422  funprg  5429  funtpg  5430  funtp  5432  fntpg  5435  fununi  5447  funcnvuni  5448  imadiflem  5458  imainlem  5460  funimaexglem  5462  isarep2  5466  fnunsn  5488  2elresin  5492  fnimadisj  5502  dmmptd  5512  fco  5550  funssxp  5555  fssres  5563  feu  5572  fimacnvdisj  5574  fabexg  5577  f00  5582  f0rn0  5585  f1co  5608  fores  5623  foco  5624  f1ores  5652  foimacnv  5655  f1oun  5657  fun11iun  5658  f1oco  5660  fo00  5675  brprcneu  5686  fv3  5716  relelfvdm  5725  nfvres  5729  nfunsn  5730  funfvbrb  5816  respreima  5830  dff2  5846  dff3im  5847  dffo4  5850  fvmptelcdm  5855  ffvresb  5865  f1oresrab  5867  fmptco  5868  fsn  5874  fcof  5888  fpr  5891  ftpg  5893  fsnunf  5909  fsnunfv  5910  elabrex  5957  dff1o6  5976  foeqcnvco  5990  fliftel1  5994  isores1  6014  isoini2  6019  riotasbc  6049  acexmidlemph  6072  acexmidlemcase  6074  oprabidlem  6110  brabvv  6128  eloprabga  6169  fnoprabg  6183  caovimo  6277  oprabexd  6354  uchoice  6365  fo1stresm  6389  fo2ndresm  6390  unielxp  6402  1st2ndbr  6412  opabn1stprc  6423  fmpoco  6446  1stconst  6451  2ndconst  6452  poxp  6462  spc2ed  6463  disjxp1  6466  elmpom  6468  suppsnopdc  6484  reldmtpos  6518  tposfun  6525  dftpos4  6528  smores  6557  smores2  6559  tfrlem1  6573  tfr0dm  6587  tfrlemibxssdm  6592  tfrlemibex  6594  tfrlemiubacc  6595  tfrlemi14d  6598  tfrexlem  6599  tfri1d  6600  tfr1onlembxssdm  6608  tfr1onlembex  6610  tfr1onlemubacc  6611  tfr1onlemres  6614  tfrcllemsucfn  6618  tfrcllembxssdm  6621  tfrcllembex  6623  tfrcllemubacc  6624  tfrcllemres  6627  tfri3  6632  rdgon  6651  frecabcl  6664  frecfcllem  6669  frecrdg  6673  2oconcl  6706  nnsucelsuc  6758  nntri3or  6760  nndceq  6766  nndcel  6767  dcdifsnid  6771  ecexr  6806  brdifun  6828  ecelqsdm  6873  iinerm  6875  eroveu  6894  erovlem  6895  ecopovtrn  6900  ecopovtrng  6903  th3qlem1  6905  fsetdmprc0  6944  pmsspw  6958  map0b  6962  mapsnd  6964  mapsn  6966  mapsncnv  6971  ixpf  6996  uniixp  6997  ixpexgg  6998  resixp  7009  f1oen3g  7034  ssdomg  7059  domtr  7066  snfig  7097  modom  7102  enpr2d  7105  dom1o  7110  xpf1o  7138  xpmapenlem  7143  php5dom  7158  fidceq  7165  nnfi  7168  fiunsnnn  7179  findcard  7186  findcard2  7187  findcard2s  7188  ac6sfi  7196  fidcen  7197  tridc  7198  fimax2gtri  7200  finexdc  7201  elssdc  7203  eqsndc  7204  exmidpw  7209  exmidpweq  7210  exmidpw2en  7213  nnwetri  7217  unsnfi  7220  unsnfidcex  7221  unsnfidcel  7222  undifdcss  7224  tpfidisj  7230  tpfidceq  7231  exmidssfi  7240  iunfidisj  7254  mapfi  7255  fissfi  7257  snexxph  7261  fidcenumlemrks  7264  sbthlem2  7269  sbthlemi3  7270  sbthlem7  7274  sbthlemi8  7275  fival  7298  dcfi  7309  fdcf1  7310  f1setfi  7311  supmoti  7327  djuss  7404  updjudhf  7413  updjud  7416  casefun  7419  caseinj  7423  omp1eomlem  7428  djufun  7438  djuinj  7440  ctssdccl  7445  ctfoex  7452  nnnninf  7460  nnnninfeq2  7463  nninfisollem0  7464  nninfisollemne  7465  nninfisollemeq  7466  nninfisol  7467  finomni  7474  exmidomniim  7475  exmidomni  7476  fodjuomnilemdc  7478  omniwomnimkv  7501  nninfdcinf  7505  nninfwlporlem  7507  nninfwlpoimlemg  7509  nninfwlpoim  7513  nninfinfwlpo  7514  exmidonfinlem  7539  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  finacn  7554  exmidaclem  7558  dju1en  7563  exmidontriimlem1  7571  exmidontriimlem3  7573  iftrueb01  7576  pw1on  7579  3nsssucpw1  7589  2omotaplemap  7617  2omotap  7619  exmidmotap  7621  cc4f  7629  cc4n  7631  acnccim  7632  dmaddpqlem  7738  nqpi  7739  dmaddpq  7740  dmmulpq  7741  ltdcnq  7758  subhalfnqq  7775  enq0sym  7793  enq0ref  7794  enq0tr  7795  nqnq0pi  7799  nq0nn  7803  addnq0mo  7808  mulnq0mo  7809  nqpnq0nq  7814  nqnq0a  7815  nqnq0m  7816  npsspw  7832  elnp1st2nd  7837  prnmaxl  7849  prnminu  7850  prarloc  7864  genprndl  7882  genprndu  7883  nqprm  7903  nqprl  7912  nqpru  7913  addnqprlemrl  7918  addnqprlemru  7919  prmuloc  7927  mulnqprlemrl  7934  mulnqprlemru  7935  ltsopr  7957  ltexprlemm  7961  ltexprlemopl  7962  ltexprlemopu  7964  lteupri  7978  recexprlemopl  7986  recexprlemopu  7988  recexprlemdisj  7991  archpr  8004  cauappcvgprlemdisj  8012  cauappcvgprlemladdrl  8018  cauappcvgprlem2  8021  caucvgprlemnbj  8028  caucvgprlemdisj  8035  caucvgprlemladdfu  8038  caucvgprlem2  8041  caucvgprprlemnbj  8054  caucvgprprlemdisj  8063  suplocexprlemml  8077  suplocexprlemrl  8078  suplocexprlemmu  8079  suplocexprlemloc  8082  addsrmo  8104  mulsrmo  8105  recexgt0sr  8134  prsrpos  8146  caucvgsrlemasr  8151  suplocsrlemb  8167  suplocsrlempr  8168  suplocsr  8170  elrealeu  8190  pitonn  8209  pitoregt0  8210  pitore  8211  recnnre  8212  axaddcl  8225  axaddrcl  8226  axmulcl  8227  axmulrcl  8228  axrnegex  8240  axcnre  8242  axpre-lttrn  8245  rereceu  8250  axarch  8252  axpre-suploclemres  8262  axpre-suploc  8263  ltxrlt  8385  apirr  8927  divmulasscomap  9020  rerecclap  9054  lbreu  9269  arch  9543  0mnnnnn0  9578  nnm1nn0  9587  elnnnn0c  9591  elnnz1  9650  ztri3or0  9669  nzadd  9680  nn0n0n1ge2  9698  zdceq  9703  zdcle  9704  zdclt  9705  uzind  9740  eluzge3nn  9955  supinfneg  9978  infsupneg  9979  eluz2b2  9986  elnn1uz2  9990  elnn0dc  9994  elnndc  9995  nn01to3  10000  znq  10007  qaddcl  10018  qmulcl  10020  qreccl  10025  irradd  10029  irrmul  10030  elpq  10032  cnref1o  10034  xnn0dcle  10187  xrpnfdc  10227  xrmnfdc  10228  xaddcom  10246  xnegdi  10253  xpncan  10256  xleadd1a  10258  iooidg  10294  elioo4g  10319  elfzd  10402  fzdcel  10427  fznlem  10428  fzpreddisj  10461  fz0to4untppr  10514  elfz0ubfz0  10515  elfz0fzfz0  10516  fz0fzelfz0  10517  fz0fzdiffz0  10520  elfzmlbp  10522  difelfzle  10524  4fvwrd4  10530  fzosplit  10569  elfzo0  10576  nn0p1elfzo  10577  fzo1fzo0n0  10578  elfzonn0  10581  fzofzim  10583  elfzo1  10586  elfzom1elp1fzo  10603  fzossfzop1  10613  ssfzo12bi  10626  exfzdc  10642  zsupcllemstep  10645  infssuzex  10649  qdceq  10662  qdclt  10663  exbtwnzlemstep  10665  exbtwnzlemex  10667  exbtwnz  10668  rebtwn2zlemstep  10670  rebtwn2z  10672  qbtwnxr  10675  modfzo0difsn  10815  frec2uzrand  10825  frec2uzf1od  10826  frecuzrdgrcl  10830  frecuzrdgtcl  10832  frecuzrdgrclt  10835  frecuzrdgfunlem  10839  frecfzennn  10846  nninfinf  10863  seq3f1olemp  10935  seq3f1oleml  10936  seqf1oglem1  10939  ser0f  10954  expcl2lemap  10971  hashunsng  11231  hashmap  11251  sshashneg  11264  hashfibclem  11265  hashfibc  11266  hashf1lem1  11268  hashf1lem2  11269  iswrdinn0  11292  snopiswrd  11297  wrdlndm  11304  iswrdsymb  11305  wrdsymb1  11324  ccatfv0  11354  ccatval21sw  11356  lswccatn0lsw  11362  eqs1  11379  ccat1st1st  11392  lswccats1fst  11395  fzowrddc  11402  swrdfv0  11409  swrdlen2  11417  swrdfv2  11418  swrdsbslen  11421  swrdspsleq  11422  pfxfv0  11447  pfxtrcfv0  11449  pfxeq  11451  pfx1  11458  swrdswrdlem  11459  cats1un  11476  pfxccatin12lem2a  11482  pfxccatin12lem2  11486  pfxccatin12lem3  11487  swrdccat  11490  cats1fvn  11519  cats1fvnd  11520  shftfvalg  11566  shftfval  11569  caucvgre  11730  rexanuz  11737  recvguniq  11744  rennim  11751  resqrexlemf  11756  rsqrmo  11776  fimaxre2  11976  climeu  12045  sumdc  12107  summodc  12133  zsumdc  12134  isum  12135  fisumss  12142  isumss2  12143  fsumsplit  12157  sumsnf  12159  fsumsplitsn  12160  sumtp  12164  sumsplitdc  12182  fsum2dlemstep  12184  fisum0diag2  12197  fsumconst  12204  modfsummodlemstep  12207  fsum00  12212  fsumabs  12215  fsumiun  12227  isumlessdc  12246  expcnv  12254  prodmodc  12328  zproddc  12329  iprodap  12330  iprodap0  12332  fprodssdc  12340  prodsnf  12342  fprodsplitdc  12346  fprodsplit  12347  fprodm1  12348  fprod1p  12349  fprodunsn  12354  fprod2dlemstep  12372  fprodsplitsn  12383  ef0lem  12410  modmulconst  12573  dvdsdivcl  12600  dvdsssfz1  12602  dvdsfac  12610  zeoxor  12619  nn0ehalf  12653  nn0oddm1d2  12659  nnoddm1d2  12660  divalglemeunn  12671  divalglemeuneg  12673  bitsfzolem  12704  bitsinv1  12712  gcdsupex  12717  gcdsupcl  12718  bezoutlemnewy  12756  bezoutlemmain  12758  bezoutlemeu  12767  dfgcd2  12774  nnwosdc  12799  nninfct  12801  algrf  12806  algcvgblem  12810  lcmgcdlem  12838  lcmdvds  12840  coprmgcdb  12849  mulgcddvds  12855  qredeu  12858  cncongr1  12864  cncongr2  12865  isprm2lem  12877  dvdsnprmd  12886  prmdc  12891  oddprmge3  12896  pw2dvdseu  12929  phibndlem  12977  dfphi2  12981  hashdvds  12982  phiprmpw  12983  eulerthlemh  12992  hashgcdeq  13001  phisum  13002  odzdvds  13007  reumodprminv  13015  nnnn0modprm0  13017  prm23ge5  13026  pclemdc  13050  pcdvdsb  13082  difsqpwdvds  13100  oddprmdvds  13116  1arith  13129  4sqlem3  13152  4sqlemafi  13157  4sqlemffi  13158  4sqleminfi  13159  4sqexercise1  13160  4sqlem11  13163  4sqlem19  13171  ballotfilemcdc  13206  ballotfilemdifcfi  13208  ballotfilemdifcfz  13210  ballotfilem2  13211  ballotfilemiex  13227  ballotfilemscl  13230  ballotfilemth  13264  ennnfonelemdc  13273  ennnfonelemh  13278  ennnfonelemhf1o  13287  ennnfonelemf1  13292  ennnfonelemrn  13293  ennnfonelemdm  13294  exmidunben  13300  ctinfomlemom  13301  ctinfom  13302  ctiunctlemudc  13311  ctiunctlemf  13312  ctiunctal  13315  nninfdclemcl  13322  nninfdclemf  13323  nninfdclemp1  13324  isstructim  13349  setsresg  13373  strleund  13440  1strbas  13454  2strbasg  13457  2stropg  13458  restsspw  13586  tgval  13599  ptex  13601  imasaddfnlemg  13618  fnpr2o  13643  fnpr2ob  13644  mgmidsssn0  13687  fngzsum  13691  gzsumvalx  13692  isnsgrp  13704  sgrpidmndm  13716  mndinvmod  13741  mnd1  13745  mhmeql  13782  grpinveu  13826  mulgval  13908  subgintm  13984  trivsubgsnd  13987  eqgfval  14008  ecqusaddd  14024  ecqusaddcl  14025  ghmeql  14053  iscmnd  14084  imasabl  14123  gzsummhm2  14129  gsump1  14140  gsummhm2fi  14148  prdsinvlem  14179  rnglz  14227  srgfcl  14260  rhmopp  14466  opprlring  14487  subrgdvds  14526  lssuni  14683  lssintclm  14704  lspf  14709  qusmulrng  14852  mulgrhm2  14928  znf1o  14969  aspid  15000  psrbagfi  15042  psrbagconcl  15046  psr1clfi  15062  mplsubgfilemcl  15073  istopon  15097  toponcom  15111  topgele  15113  topontopn  15121  tsettps  15122  eltg2b  15138  unitg  15146  tgss2  15163  bastop2  15168  distop  15169  epttop  15174  cldss2  15190  neisspw  15232  neipsm  15238  neiuni  15245  tgcn  15292  tgcnp  15293  cnntr  15309  lmff  15333  txuni2  15340  txbasex  15341  txbas  15342  txcnp  15355  txcnmpt  15357  txcn  15359  txdis  15361  txdis1cn  15362  cnmpt11  15367  cnmpt12  15371  cnmpt21  15375  cnmpt2t  15377  cnmpt22  15378  blsscls2  15577  xmetxpbl  15592  xmettxlem  15593  tgqioo  15639  fsumcncntop  15651  cncfmpt1f  15682  mulcncflem  15691  mulcncf  15692  dedekindeu  15707  dedekindicclemicc  15716  dedekindicc  15717  ivthinclemdisj  15724  hovercncf  15730  limcimo  15749  cnmptlimc  15758  reldvg  15763  dvfvalap  15765  dvfgg  15772  dvmptfsum  15809  dveflem  15810  dvef  15811  elply2  15819  sincn  15853  coscn  15854  reeff1o  15857  pilem3  15867  ioocosf1o  15938  mpodvdsmulf1o  16087  fsumdvdsmul  16088  perfectlem2  16097  lgsne0  16140  gausslemma2dlem1a  16160  gausslemma2dlem4  16166  lgseisenlem2  16173  lgseisenlem3  16174  lgsquadlem2  16180  2lgslem3  16203  2sqlem2  16217  mul2sq  16218  2sqlem3  16219  2sqlem7  16223  edgstruct  16288  pw0ss  16307  incistruhgr  16314  upgrex  16327  umgrnloop0  16341  upgr1een  16348  lfgrnloopen  16357  umgredg  16369  umgrnloop2  16375  uspgredgiedg  16402  uspgriedgedg  16403  usgrislfuspgrdom  16414  usgredg3  16438  uspgredg2vlem  16444  uspgredg2v  16445  ushgredgedg  16450  ushgredgedgloop  16452  uhgr0vsize0en  16459  usgr1e  16465  subusgr  16499  vtxedgfi  16513  vtxlpfi  16514  vtxdumgrfival  16522  1loopgrvd2fi  16529  p1evtxdeqfilem  16535  vdegp1aid  16538  wlkcprim  16574  wlk1walkdom  16583  uspgr2wlkeq  16589  upgr2wlkdc  16601  wlkres  16603  clwwlkccatlem  16624  clwwlknp  16641  umgr2cwwk2dif  16648  trlsegvdegfi  16691  eupth2lem3lem3fi  16694  eupth2lem3lem6fi  16695  eupth2lem3lem4fi  16697  eupth2lembfi  16701  depindlem1  16730  bj-trst  16750  bj-fast  16752  bj-stand  16759  bj-trdc  16763  bj-fadc  16765  decidr  16807  djulclALT  16812  djurclALT  16813  bj-charfunr  16819  bj-indind  16941  bj-2inf  16947  bj-nntrans2  16961  bj-peano4  16964  bj-nnord  16967  bj-inf2vn  16983  bj-inf2vn2  16984  bj-findis  16988  pwf1oexmid  17012  subctctexmid  17013  pw1dceq  17017  exmidnotnotr  17018  exmidcon  17019  exmidpeirce  17020  nnsf  17022  nninfsellemdc  17027  nninffeq  17037  nnnninfen  17038  exmidsbthrlem  17041  sbthom  17045  triap  17052  trilpo  17066  apdifflemr  17070  redcwlpo  17079  tridceq  17080  nconstwlpolem0  17087  nconstwlpolem  17089  nconstwlpo  17090  neapmkv  17092  ltlenmkv  17094