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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3772  rabsnif  3778  absneu  3783  rabsneu  3784  opprc  3925  elunii  3940  dfnfc2  3953  uniss2  3966  unidif  3967  ssunieq  3968  intab  3999  iunss2  4057  iunssd  4058  iunxdif2  4061  invdisj  4123  disjiun  4125  3brtr4g  4164  trin  4239  triun  4242  truni  4243  trint  4244  iinexgm  4290  class2seteq  4300  pwuni  4329  exmid1dc  4337  exmidn0m  4338  exmidsssn  4339  exmid0el  4341  exmidel  4342  exmidundif  4343  exmidundifim  4344  exmid1stab  4345  mss  4366  copsex2t  4385  euotd  4395  pwunim  4431  ispod  4449  sotricim  4468  exse  4481  frind  4497  trssord  4525  suctr  4566  pwnex  4595  eusvnf  4599  eusvnfb  4600  eusv2nf  4602  rexxfrd  4609  ralxfr2d  4610  rexxfr2d  4611  rabxfrd  4615  reuhypd  4617  eldifpw  4623  iunpw  4626  ssorduni  4634  onsucb  4650  onsucelsucr  4655  sucunielr  4657  ontriexmidim  4669  ordtri2or2exmidlem  4673  onsucelsucexmid  4677  reg2exmidlema  4681  setindel  4685  elirr  4688  orddisj  4693  en2lp  4701  suc11g  4704  ordsuc  4710  nlimsucg  4713  ordtri2or2exmid  4718  ontri2orexmidim  4719  zfregfr  4721  wessep  4725  tfi  4729  peano5  4745  limom  4761  peano2b  4762  nndceq0  4765  nnpredcl  4770  0nelrel  4821  eqrelrdv  4871  xpsspw  4887  relint  4901  relop  4930  eqbrrdva  4950  ssrelrn  4972  opeldm  4984  reldmm  5000  elres  5099  relssres  5101  elrelimasn  5153  exse2  5161  issref  5170  trin2  5179  dminss  5202  imainss  5203  rnxpid  5222  dmsn0el  5257  dmmptg  5285  relrelss  5314  cnviinm  5329  iotanul  5353  sniota  5368  dffun5r  5389  funmo  5392  funco  5417  funun  5422  fununmo  5423  fununfun  5424  funprg  5431  funtpg  5432  funtp  5434  fntpg  5437  fununi  5449  funcnvuni  5450  imadiflem  5460  imainlem  5462  funimaexglem  5464  isarep2  5468  fnunsn  5490  2elresin  5494  fnimadisj  5504  dmmptd  5514  fco  5552  funssxp  5557  fssres  5565  feu  5574  fimacnvdisj  5576  fabexg  5579  f00  5584  f0rn0  5587  f1co  5610  fores  5625  foco  5626  f1ores  5654  foimacnv  5657  f1oun  5659  fun11iun  5660  f1oco  5662  fo00  5677  brprcneu  5688  fv3  5718  relelfvdm  5727  nfvres  5732  nfunsn  5733  funfvbrb  5822  respreima  5836  dff2  5852  dff3im  5853  dffo4  5856  fvmptelcdm  5861  ffvresb  5871  f1oresrab  5873  fmptco  5874  fsn  5880  fcof  5894  fpr  5897  ftpg  5899  fsnunf  5915  fsnunfv  5916  elabrex  5963  dff1o6  5982  foeqcnvco  5996  fliftel1  6000  isores1  6020  isoini2  6025  riotasbc  6055  acexmidlemph  6078  acexmidlemcase  6080  oprabidlem  6116  brabvv  6134  eloprabga  6175  fnoprabg  6189  caovimo  6283  oprabexd  6360  uchoice  6371  fo1stresm  6395  fo2ndresm  6396  unielxp  6408  1st2ndbr  6418  opabn1stprc  6429  fmpoco  6452  1stconst  6457  2ndconst  6458  poxp  6468  spc2ed  6469  disjxp1  6472  elmpom  6474  suppsnopdc  6490  reldmtpos  6524  tposfun  6531  dftpos4  6534  smores  6563  smores2  6565  tfrlem1  6579  tfr0dm  6593  tfrlemibxssdm  6598  tfrlemibex  6600  tfrlemiubacc  6601  tfrlemi14d  6604  tfrexlem  6605  tfri1d  6606  tfr1onlembxssdm  6614  tfr1onlembex  6616  tfr1onlemubacc  6617  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllembxssdm  6627  tfrcllembex  6629  tfrcllemubacc  6630  tfrcllemres  6633  tfri3  6638  rdgon  6657  frecabcl  6670  frecfcllem  6675  frecrdg  6679  2oconcl  6712  nnsucelsuc  6764  nntri3or  6766  nndceq  6772  nndcel  6773  dcdifsnid  6777  ecexr  6812  brdifun  6834  ecelqsdm  6879  iinerm  6881  eroveu  6900  erovlem  6901  ecopovtrn  6906  ecopovtrng  6909  th3qlem1  6911  fsetdmprc0  6950  pmsspw  6964  map0b  6968  mapsnd  6970  mapsn  6972  mapsncnv  6977  ixpf  7002  uniixp  7003  ixpexgg  7004  resixp  7015  f1oen3g  7040  ssdomg  7065  domtr  7072  snfig  7103  modom  7108  enpr2d  7111  dom1o  7116  xpf1o  7144  xpmapenlem  7149  php5dom  7164  fidceq  7171  nnfi  7174  fiunsnnn  7185  findcard  7192  findcard2  7193  findcard2s  7194  ac6sfi  7202  fidcen  7203  tridc  7204  fimax2gtri  7206  finexdc  7207  elssdc  7209  eqsndc  7210  exmidpw  7215  exmidpweq  7216  exmidpw2en  7219  nnwetri  7223  unsnfi  7226  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  tpfidisj  7236  tpfidceq  7237  exmidssfi  7246  iunfidisj  7260  mapfi  7261  fissfi  7263  snexxph  7267  fidcenumlemrks  7270  sbthlem2  7275  sbthlemi3  7276  sbthlem7  7280  sbthlemi8  7281  fival  7304  dcfi  7315  fdcf1  7316  f1setfi  7317  supmoti  7333  djuss  7410  updjudhf  7419  updjud  7422  casefun  7425  caseinj  7429  omp1eomlem  7434  djufun  7444  djuinj  7446  ctssdccl  7451  ctfoex  7458  nnnninf  7466  nnnninfeq2  7469  nninfisollem0  7470  nninfisollemne  7471  nninfisollemeq  7472  nninfisol  7473  finomni  7480  exmidomniim  7481  exmidomni  7482  fodjuomnilemdc  7484  omniwomnimkv  7507  nninfdcinf  7511  nninfwlporlem  7513  nninfwlpoimlemg  7515  nninfwlpoim  7519  nninfinfwlpo  7520  exmidonfinlem  7545  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  finacn  7560  exmidaclem  7564  dju1en  7569  exmidontriimlem1  7577  exmidontriimlem3  7579  iftrueb01  7582  pw1on  7585  3nsssucpw1  7595  2omotaplemap  7623  2omotap  7625  exmidmotap  7627  cc4f  7635  cc4n  7637  acnccim  7638  dmaddpqlem  7744  nqpi  7745  dmaddpq  7746  dmmulpq  7747  ltdcnq  7764  subhalfnqq  7781  enq0sym  7799  enq0ref  7800  enq0tr  7801  nqnq0pi  7805  nq0nn  7809  addnq0mo  7814  mulnq0mo  7815  nqpnq0nq  7820  nqnq0a  7821  nqnq0m  7822  npsspw  7838  elnp1st2nd  7843  prnmaxl  7855  prnminu  7856  prarloc  7870  genprndl  7888  genprndu  7889  nqprm  7909  nqprl  7918  nqpru  7919  addnqprlemrl  7924  addnqprlemru  7925  prmuloc  7933  mulnqprlemrl  7940  mulnqprlemru  7941  ltsopr  7963  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemopu  7970  lteupri  7984  recexprlemopl  7992  recexprlemopu  7994  recexprlemdisj  7997  archpr  8010  cauappcvgprlemdisj  8018  cauappcvgprlemladdrl  8024  cauappcvgprlem2  8027  caucvgprlemnbj  8034  caucvgprlemdisj  8041  caucvgprlemladdfu  8044  caucvgprlem2  8047  caucvgprprlemnbj  8060  caucvgprprlemdisj  8069  suplocexprlemml  8083  suplocexprlemrl  8084  suplocexprlemmu  8085  suplocexprlemloc  8088  addsrmo  8110  mulsrmo  8111  recexgt0sr  8140  prsrpos  8152  caucvgsrlemasr  8157  suplocsrlemb  8173  suplocsrlempr  8174  suplocsr  8176  elrealeu  8196  pitonn  8215  pitoregt0  8216  pitore  8217  recnnre  8218  axaddcl  8231  axaddrcl  8232  axmulcl  8233  axmulrcl  8234  axrnegex  8246  axcnre  8248  axpre-lttrn  8251  rereceu  8256  axarch  8258  axpre-suploclemres  8268  axpre-suploc  8269  ltxrlt  8391  apirr  8934  divmulasscomap  9027  rerecclap  9061  lbreu  9276  indconst1  9304  arch  9562  0mnnnnn0  9597  nnm1nn0  9606  elnnnn0c  9610  elnnz1  9669  ztri3or0  9688  nzadd  9699  nn0n0n1ge2  9717  zdceq  9722  zdcle  9723  zdclt  9724  uzind  9759  eluzge3nn  9974  supinfneg  9997  infsupneg  9998  eluz2b2  10005  elnn1uz2  10009  elnn0dc  10013  elnndc  10014  nn01to3  10019  znq  10026  qaddcl  10037  qmulcl  10039  qreccl  10044  irradd  10048  irrmul  10049  elpq  10051  cnref1o  10053  xnn0dcle  10206  xrpnfdc  10246  xrmnfdc  10247  xaddcom  10265  xnegdi  10272  xpncan  10275  xleadd1a  10277  iooidg  10313  elioo4g  10338  elfzd  10421  fzdcel  10446  fznlem  10447  fzpreddisj  10480  fz0to4untppr  10533  elfz0ubfz0  10534  elfz0fzfz0  10535  fz0fzelfz0  10536  fz0fzdiffz0  10539  elfzmlbp  10541  difelfzle  10543  4fvwrd4  10549  fzosplit  10588  elfzo0  10595  nn0p1elfzo  10596  fzo1fzo0n0  10597  elfzonn0  10600  fzofzim  10602  elfzo1  10605  elfzom1elp1fzo  10622  fzossfzop1  10632  ssfzo12bi  10645  exfzdc  10661  zsupcllemstep  10664  infssuzex  10668  qdceq  10681  qdclt  10682  exbtwnzlemstep  10684  exbtwnzlemex  10686  exbtwnz  10687  rebtwn2zlemstep  10689  rebtwn2z  10691  qbtwnxr  10694  modfzo0difsn  10834  frec2uzrand  10844  frec2uzf1od  10845  frecuzrdgrcl  10849  frecuzrdgtcl  10851  frecuzrdgrclt  10854  frecuzrdgfunlem  10858  frecfzennn  10865  nninfinf  10882  seq3f1olemp  10954  seq3f1oleml  10955  seqf1oglem1  10958  ser0f  10973  expcl2lemap  10990  hashunsng  11250  hashmap  11270  sshashneg  11283  hashfibclem  11284  hashfibc  11285  hashf1lem1  11287  hashf1lem2  11288  iswrdinn0  11311  snopiswrd  11316  wrdlndm  11323  iswrdsymb  11324  wrdsymb1  11343  ccatfv0  11373  ccatval21sw  11375  lswccatn0lsw  11381  eqs1  11398  ccat1st1st  11411  lswccats1fst  11414  fzowrddc  11421  swrdfv0  11428  swrdlen2  11436  swrdfv2  11437  swrdsbslen  11440  swrdspsleq  11441  pfxfv0  11466  pfxtrcfv0  11468  pfxeq  11470  pfx1  11477  swrdswrdlem  11478  cats1un  11495  pfxccatin12lem2a  11501  pfxccatin12lem2  11505  pfxccatin12lem3  11506  swrdccat  11509  cats1fvn  11538  cats1fvnd  11539  shftfvalg  11585  shftfval  11588  caucvgre  11749  rexanuz  11756  recvguniq  11763  rennim  11770  resqrexlemf  11775  rsqrmo  11795  fimaxre2  11995  climeu  12064  sumdc  12126  summodc  12152  zsumdc  12153  isum  12154  fisumss  12161  isumss2  12162  fsumsplit  12176  sumsnf  12178  fsumsplitsn  12179  sumtp  12183  sumsplitdc  12201  fsum2dlemstep  12203  fisum0diag2  12216  fsumconst  12223  modfsummodlemstep  12226  fsum00  12231  fsumabs  12234  fsumiun  12246  isumlessdc  12265  expcnv  12273  prodmodc  12347  zproddc  12348  iprodap  12349  iprodap0  12351  fprodssdc  12359  prodsnf  12361  fprodsplitdc  12365  fprodsplit  12366  fprodm1  12367  fprod1p  12368  fprodunsn  12373  fprod2dlemstep  12391  fprodsplitsn  12402  ef0lem  12429  modmulconst  12592  dvdsdivcl  12619  dvdsssfz1  12621  dvdsfac  12629  zeoxor  12638  nn0ehalf  12672  nn0oddm1d2  12678  nnoddm1d2  12679  divalglemeunn  12690  divalglemeuneg  12692  bitsfzolem  12723  bitsinv1  12731  gcdsupex  12736  gcdsupcl  12737  bezoutlemnewy  12775  bezoutlemmain  12777  bezoutlemeu  12786  dfgcd2  12793  nnwosdc  12818  nninfct  12820  algrf  12825  algcvgblem  12829  lcmgcdlem  12857  lcmdvds  12859  coprmgcdb  12868  mulgcddvds  12874  qredeu  12877  cncongr1  12883  cncongr2  12884  isprm2lem  12896  dvdsnprmd  12905  prmdc  12910  oddprmge3  12915  pw2dvdseu  12948  phibndlem  12996  dfphi2  13000  hashdvds  13001  phiprmpw  13002  eulerthlemh  13011  hashgcdeq  13020  phisum  13021  odzdvds  13026  reumodprminv  13034  nnnn0modprm0  13036  prm23ge5  13045  pclemdc  13069  pcdvdsb  13101  difsqpwdvds  13119  oddprmdvds  13135  1arith  13148  4sqlem3  13171  4sqlemafi  13176  4sqlemffi  13177  4sqleminfi  13178  4sqexercise1  13179  4sqlem11  13182  4sqlem19  13190  ballotfilemcdc  13225  ballotfilemdifcfi  13227  ballotfilemdifcfz  13229  ballotfilem2  13230  ballotfilemiex  13246  ballotfilemscl  13249  ballotfilemth  13283  ennnfonelemdc  13292  ennnfonelemh  13297  ennnfonelemhf1o  13306  ennnfonelemf1  13311  ennnfonelemrn  13312  ennnfonelemdm  13313  exmidunben  13319  ctinfomlemom  13320  ctinfom  13321  ctiunctlemudc  13330  ctiunctlemf  13331  ctiunctal  13334  nninfdclemcl  13341  nninfdclemf  13342  nninfdclemp1  13343  isstructim  13368  setsresg  13392  strleund  13459  1strbas  13473  2strbasg  13476  2stropg  13477  restsspw  13605  tgval  13618  ptex  13620  imasaddfnlemg  13637  fnpr2o  13662  fnpr2ob  13663  mgmidsssn0  13706  fngzsum  13710  gzsumvalx  13711  isnsgrp  13723  sgrpidmndm  13735  mndinvmod  13760  mnd1  13764  mhmeql  13801  grpinveu  13845  mulgval  13927  subgintm  14003  trivsubgsnd  14006  eqgfval  14027  ecqusaddd  14043  ecqusaddcl  14044  ghmeql  14072  iscmnd  14103  imasabl  14142  gzsummhm2  14148  gsump1  14159  gsummhm2fi  14167  prdsinvlem  14198  rnglz  14246  srgfcl  14279  rhmopp  14485  opprlring  14506  subrgdvds  14545  lssuni  14702  lssintclm  14723  lspf  14728  qusmulrng  14871  mulgrhm2  14947  znf1o  14988  aspid  15019  psrbagfi  15061  psrbagconcl  15065  psr1clfi  15081  mplsubgfilemcl  15092  istopon  15116  toponcom  15130  topgele  15132  topontopn  15140  tsettps  15141  eltg2b  15157  unitg  15165  tgss2  15182  bastop2  15187  distop  15188  epttop  15193  cldss2  15209  neisspw  15251  neipsm  15257  neiuni  15264  tgcn  15311  tgcnp  15312  cnntr  15328  lmff  15352  txuni2  15359  txbasex  15360  txbas  15361  txcnp  15374  txcnmpt  15376  txcn  15378  txdis  15380  txdis1cn  15381  cnmpt11  15386  cnmpt12  15390  cnmpt21  15394  cnmpt2t  15396  cnmpt22  15397  blsscls2  15596  xmetxpbl  15611  xmettxlem  15612  tgqioo  15658  fsumcncntop  15670  cncfmpt1f  15701  mulcncflem  15710  mulcncf  15711  dedekindeu  15726  dedekindicclemicc  15735  dedekindicc  15736  ivthinclemdisj  15743  hovercncf  15749  limcimo  15768  cnmptlimc  15777  reldvg  15782  dvfvalap  15784  dvfgg  15791  dvmptfsum  15828  dveflem  15829  dvef  15830  elply2  15838  sincn  15872  coscn  15873  reeff1o  15876  pilem3  15887  ioocosf1o  15958  mpodvdsmulf1o  16110  fsumdvdsmul  16111  perfectlem2  16120  bcmono  16124  lgsne0  16169  gausslemma2dlem1a  16189  gausslemma2dlem4  16195  lgseisenlem2  16202  lgseisenlem3  16203  lgsquadlem2  16209  2lgslem3  16232  2sqlem2  16246  mul2sq  16247  2sqlem3  16248  2sqlem7  16252  edgstruct  16317  pw0ss  16336  incistruhgr  16343  upgrex  16356  umgrnloop0  16370  upgr1een  16377  lfgrnloopen  16386  umgredg  16398  umgrnloop2  16404  uspgredgiedg  16431  uspgriedgedg  16432  usgrislfuspgrdom  16443  usgredg3  16467  uspgredg2vlem  16473  uspgredg2v  16474  ushgredgedg  16479  ushgredgedgloop  16481  uhgr0vsize0en  16488  usgr1e  16494  subusgr  16528  vtxedgfi  16542  vtxlpfi  16543  vtxdumgrfival  16551  1loopgrvd2fi  16558  p1evtxdeqfilem  16564  vdegp1aid  16567  wlkcprim  16603  wlk1walkdom  16612  uspgr2wlkeq  16618  upgr2wlkdc  16630  wlkres  16632  clwwlkccatlem  16653  clwwlknp  16670  umgr2cwwk2dif  16677  trlsegvdegfi  16720  eupth2lem3lem3fi  16723  eupth2lem3lem6fi  16724  eupth2lem3lem4fi  16726  eupth2lembfi  16730  depindlem1  16759  bj-trst  16779  bj-fast  16781  bj-stand  16788  bj-trdc  16792  bj-fadc  16794  decidr  16836  djulclALT  16841  djurclALT  16842  bj-charfunr  16848  bj-indind  16970  bj-2inf  16976  bj-nntrans2  16990  bj-peano4  16993  bj-nnord  16996  bj-inf2vn  17012  bj-inf2vn2  17013  bj-findis  17017  pwf1oexmid  17041  subctctexmid  17042  pw1dceq  17047  exmidnotnotr  17048  exmidcon  17049  exmidpeirce  17050  wexmiddc  17054  wexmiddiffi  17056  wexmiddifxylem  17057  wexmiddifxy  17058  nnsf  17060  nninfsellemdc  17065  nninffeq  17075  nnnninfen  17076  exmidsbthrlem  17079  sbthom  17083  triap  17090  trilpo  17104  apdifflemr  17108  redcwlpo  17117  tridceq  17118  nconstwlpolem0  17125  nconstwlpolem  17127  nconstwlpo  17128  neapmkv  17130  ltlenmkv  17132