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  718  dcim  845  dcstab  848  stdcndc  849  stdcndcOLD  850  dcand  937  dcor  940  3mix1  1171  3mix2  1172  3jca  1182  syl3anbrc  1186  syl21anbrc  1187  inegd  1394  pclem6  1396  xoranor  1399  dcfrompeirce  1472  nfxfrd  1501  nfd  1549  hban  1573  nfan1  1590  nford  1593  nfand  1594  hbim1  1596  nfal  1602  alexim  1671  nnal  1675  ax6blem  1676  nf4r  1697  19.34  1710  nfexd  1787  sbcof2  1836  nfsb2or  1863  sbidm  1877  nfdv  1903  nfd2  2053  nfeudv  2072  mon  2086  eumo  2089  mo23  2099  eu2  2102  eu3h  2103  exmodc  2108  exmonim  2109  mo2r  2110  mo3h  2111  bm1.1  2194  eqrdv  2207  3eltr4g  2295  abbi2dv  2328  abbi1dv  2329  nfcd  2347  nfcxfrd  2350  dcned  2386  neqned  2387  3netr4g  2415  necon3bi  2430  necon2ai  2434  nnral  2500  alral  2555  rspe  2559  rsp2e  2561  rgen2a  2564  ralrimi  2581  r19.27v  2638  r19.28v  2639  r19.27av  2646  r19.32r  2657  nfreudxy  2685  mormo  2728  nrexrmo  2733  cgsex2g  2816  cgsex4g  2817  spc2egv  2873  spc2gv  2874  spc3egv  2875  spc3gv  2876  rspce  2882  ceqex  2910  elrab3t  2938  elrabd  2941  mosubt  2960  mo2icl  2962  reu3  2973  reu6i  2974  2rmorex  2989  sbc5  3032  rspesbca  3094  rmo2ilem  3099  sbnfc2  3165  ssrd  3209  ssrdv  3210  3sstr4g  3247  eqsstrid  3250  ss2abdv  3277  abssdv  3278  rabssdv  3284  ss2rabdv  3285  ssun1  3347  unssad  3361  unssbd  3362  ssddif  3418  uneqin  3435  indifdir  3440  undif3ss  3445  reuss2  3464  n0rf  3484  reximdva0m  3487  rabxmdc  3503  ssindif0im  3531  minel  3533  ralidm  3572  ralm  3575  dcun  3581  ifmdc  3625  disjsn2  3709  absneu  3718  rabsneu  3719  opprc  3857  elunii  3872  dfnfc2  3885  uniss2  3898  unidif  3899  ssunieq  3900  intab  3931  iunss2  3989  iunssd  3990  iunxdif2  3993  invdisj  4055  disjiun  4057  3brtr4g  4096  trin  4171  triun  4174  truni  4175  trint  4176  iinexgm  4217  class2seteq  4226  pwuni  4255  exmid1dc  4263  exmidn0m  4264  exmidsssn  4265  exmid0el  4267  exmidel  4268  exmidundif  4269  exmidundifim  4270  exmid1stab  4271  mss  4291  copsex2t  4310  euotd  4320  pwunim  4354  ispod  4372  sotricim  4391  exse  4404  frind  4420  trssord  4448  suctr  4489  pwnex  4517  eusvnf  4521  eusvnfb  4522  eusv2nf  4524  rexxfrd  4531  ralxfr2d  4532  rexxfr2d  4533  rabxfrd  4537  reuhypd  4539  eldifpw  4545  iunpw  4548  ssorduni  4556  onsucb  4572  onsucelsucr  4577  sucunielr  4579  ontriexmidim  4591  ordtri2or2exmidlem  4595  onsucelsucexmid  4599  reg2exmidlema  4603  setindel  4607  elirr  4610  orddisj  4615  en2lp  4623  suc11g  4626  ordsuc  4632  nlimsucg  4635  ordtri2or2exmid  4640  ontri2orexmidim  4641  zfregfr  4643  wessep  4647  tfi  4651  peano5  4667  limom  4683  peano2b  4684  nndceq0  4687  nnpredcl  4692  0nelrel  4742  eqrelrdv  4792  xpsspw  4808  relint  4820  relop  4849  eqbrrdva  4869  ssrelrn  4891  opeldm  4903  elres  5017  relssres  5019  elrelimasn  5070  exse2  5078  issref  5087  trin2  5096  dminss  5119  imainss  5120  rnxpid  5139  dmsn0el  5174  dmmptg  5202  relrelss  5231  cnviinm  5246  iotanul  5270  sniota  5285  dffun5r  5306  funmo  5309  funco  5334  funun  5338  fununmo  5339  fununfun  5340  funprg  5347  funtpg  5348  funtp  5350  fntpg  5353  fununi  5365  funcnvuni  5366  imadiflem  5376  imainlem  5378  funimaexglem  5380  isarep2  5384  fnunsn  5406  2elresin  5410  fnimadisj  5420  dmmptd  5430  fco  5465  funssxp  5469  fssres  5477  feu  5484  fimacnvdisj  5486  fabexg  5489  f00  5493  f0rn0  5496  f1co  5519  fores  5534  foco  5535  f1ores  5563  foimacnv  5566  f1oun  5568  fun11iun  5569  f1oco  5571  fo00  5585  brprcneu  5596  fv3  5626  relelfvdm  5635  nfvres  5637  nfunsn  5638  funfvbrb  5721  respreima  5736  dff2  5752  dff3im  5753  dffo4  5756  fvmptelcdm  5761  ffvresb  5771  f1oresrab  5773  fmptco  5774  fsn  5780  fpr  5794  ftpg  5796  fsnunf  5812  fsnunfv  5813  elabrex  5854  dff1o6  5873  foeqcnvco  5887  fliftel1  5891  isores1  5911  isoini2  5916  riotasbc  5944  acexmidlemph  5967  acexmidlemcase  5969  oprabidlem  6005  brabvv  6021  eloprabga  6062  fnoprabg  6076  caovimo  6170  oprabexd  6242  uchoice  6253  fo1stresm  6277  fo2ndresm  6278  unielxp  6290  1st2ndbr  6300  fmpoco  6332  1stconst  6337  2ndconst  6338  poxp  6348  spc2ed  6349  disjxp1  6352  reldmtpos  6369  tposfun  6376  dftpos4  6379  smores  6408  smores2  6410  tfrlem1  6424  tfr0dm  6438  tfrlemibxssdm  6443  tfrlemibex  6445  tfrlemiubacc  6446  tfrlemi14d  6449  tfrexlem  6450  tfri1d  6451  tfr1onlembxssdm  6459  tfr1onlembex  6461  tfr1onlemubacc  6462  tfr1onlemres  6465  tfrcllemsucfn  6469  tfrcllembxssdm  6472  tfrcllembex  6474  tfrcllemubacc  6475  tfrcllemres  6478  tfri3  6483  rdgon  6502  frecabcl  6515  frecfcllem  6520  frecrdg  6524  2oconcl  6555  nnsucelsuc  6607  nntri3or  6609  nndceq  6615  nndcel  6616  dcdifsnid  6620  ecexr  6655  brdifun  6677  ecelqsdm  6722  iinerm  6724  eroveu  6743  erovlem  6744  ecopovtrn  6749  ecopovtrng  6752  th3qlem1  6754  pmsspw  6800  map0b  6804  mapsn  6807  mapsncnv  6812  ixpf  6837  uniixp  6838  ixpexgg  6839  resixp  6850  f1oen3g  6875  ssdomg  6900  domtr  6907  snfig  6937  enpr2d  6942  xpf1o  6973  xpmapenlem  6978  php5dom  6992  fidceq  6999  nnfi  7002  fiunsnnn  7011  findcard  7018  findcard2  7019  findcard2s  7020  ac6sfi  7028  tridc  7029  fimax2gtri  7031  finexdc  7032  exmidpw  7038  exmidpweq  7039  exmidpw2en  7042  nnwetri  7046  unsnfi  7049  unsnfidcex  7050  unsnfidcel  7051  undifdcss  7053  tpfidisj  7059  tpfidceq  7060  iunfidisj  7081  snexxph  7085  fidcenumlemrks  7088  sbthlem2  7093  sbthlemi3  7094  sbthlem7  7098  sbthlemi8  7099  fival  7105  dcfi  7116  supmoti  7128  djuss  7205  updjudhf  7214  updjud  7217  casefun  7220  caseinj  7224  omp1eomlem  7229  djufun  7239  djuinj  7241  ctssdccl  7246  ctfoex  7253  nnnninf  7261  nnnninfeq2  7264  nninfisollem0  7265  nninfisollemne  7266  nninfisollemeq  7267  nninfisol  7268  finomni  7275  exmidomniim  7276  exmidomni  7277  fodjuomnilemdc  7279  omniwomnimkv  7302  nninfdcinf  7306  nninfwlporlem  7308  nninfwlpoimlemg  7310  nninfwlpoim  7314  nninfinfwlpo  7315  exmidonfinlem  7339  exmidfodomrlemr  7348  exmidfodomrlemrALT  7349  finacn  7354  exmidaclem  7358  dju1en  7363  exmidontriimlem1  7371  exmidontriimlem3  7373  iftrueb01  7376  pw1on  7379  3nsssucpw1  7389  2omotaplemap  7411  2omotap  7413  exmidmotap  7415  cc4f  7423  cc4n  7425  acnccim  7426  dmaddpqlem  7532  nqpi  7533  dmaddpq  7534  dmmulpq  7535  ltdcnq  7552  subhalfnqq  7569  enq0sym  7587  enq0ref  7588  enq0tr  7589  nqnq0pi  7593  nq0nn  7597  addnq0mo  7602  mulnq0mo  7603  nqpnq0nq  7608  nqnq0a  7609  nqnq0m  7610  npsspw  7626  elnp1st2nd  7631  prnmaxl  7643  prnminu  7644  prarloc  7658  genprndl  7676  genprndu  7677  nqprm  7697  nqprl  7706  nqpru  7707  addnqprlemrl  7712  addnqprlemru  7713  prmuloc  7721  mulnqprlemrl  7728  mulnqprlemru  7729  ltsopr  7751  ltexprlemm  7755  ltexprlemopl  7756  ltexprlemopu  7758  lteupri  7772  recexprlemopl  7780  recexprlemopu  7782  recexprlemdisj  7785  archpr  7798  cauappcvgprlemdisj  7806  cauappcvgprlemladdrl  7812  cauappcvgprlem2  7815  caucvgprlemnbj  7822  caucvgprlemdisj  7829  caucvgprlemladdfu  7832  caucvgprlem2  7835  caucvgprprlemnbj  7848  caucvgprprlemdisj  7857  suplocexprlemml  7871  suplocexprlemrl  7872  suplocexprlemmu  7873  suplocexprlemloc  7876  addsrmo  7898  mulsrmo  7899  recexgt0sr  7928  prsrpos  7940  caucvgsrlemasr  7945  suplocsrlemb  7961  suplocsrlempr  7962  suplocsr  7964  elrealeu  7984  pitonn  8003  pitoregt0  8004  pitore  8005  recnnre  8006  axaddcl  8019  axaddrcl  8020  axmulcl  8021  axmulrcl  8022  axrnegex  8034  axcnre  8036  axpre-lttrn  8039  rereceu  8044  axarch  8046  axpre-suploclemres  8056  axpre-suploc  8057  ltxrlt  8180  apirr  8720  divmulasscomap  8811  rerecclap  8845  lbreu  9060  arch  9334  0mnnnnn0  9369  nnm1nn0  9378  elnnnn0c  9382  elnnz1  9437  ztri3or0  9456  nzadd  9467  nn0n0n1ge2  9485  zdceq  9490  zdcle  9491  zdclt  9492  uzind  9526  eluzge3nn  9735  supinfneg  9758  infsupneg  9759  eluz2b2  9766  elnn1uz2  9770  elnn0dc  9774  elnndc  9775  nn01to3  9780  znq  9787  qaddcl  9798  qmulcl  9800  qreccl  9805  irradd  9809  irrmul  9810  elpq  9812  cnref1o  9814  xnn0dcle  9966  xrpnfdc  10006  xrmnfdc  10007  xaddcom  10025  xnegdi  10032  xpncan  10035  xleadd1a  10037  iooidg  10073  elioo4g  10098  elfzd  10180  fzdcel  10204  fznlem  10205  fzpreddisj  10235  fz0to4untppr  10288  elfz0ubfz0  10289  elfz0fzfz0  10290  fz0fzelfz0  10291  fz0fzdiffz0  10294  elfzmlbp  10296  difelfzle  10298  4fvwrd4  10304  fzosplit  10343  elfzo0  10350  fzo1fzo0n0  10351  elfzonn0  10354  fzofzim  10356  elfzo1  10358  elfzom1elp1fzo  10375  fzossfzop1  10385  ssfzo12bi  10398  exfzdc  10413  zsupcllemstep  10416  infssuzex  10420  qdceq  10431  qdclt  10432  exbtwnzlemstep  10434  exbtwnzlemex  10436  exbtwnz  10437  rebtwn2zlemstep  10439  rebtwn2z  10441  qbtwnxr  10444  modfzo0difsn  10584  frec2uzrand  10594  frec2uzf1od  10595  frecuzrdgrcl  10599  frecuzrdgtcl  10601  frecuzrdgrclt  10604  frecuzrdgfunlem  10608  frecfzennn  10615  nninfinf  10632  seq3f1olemp  10704  seq3f1oleml  10705  seqf1oglem1  10708  ser0f  10723  expcl2lemap  10740  hashunsng  10996  iswrdinn0  11043  snopiswrd  11048  wrdlndm  11055  iswrdsymb  11056  wrdsymb1  11074  ccatfv0  11104  ccatval21sw  11106  lswccatn0lsw  11112  eqs1  11127  ccat1st1st  11138  lswccats1fst  11141  fzowrddc  11145  swrdfv0  11152  swrdlen2  11160  swrdfv2  11161  swrdsbslen  11164  swrdspsleq  11165  pfxfv0  11190  pfxtrcfv0  11192  pfxeq  11194  pfx1  11201  swrdswrdlem  11202  cats1un  11219  pfxccatin12lem2a  11225  pfxccatin12lem2  11229  pfxccatin12lem3  11230  swrdccat  11233  cats1fvn  11262  cats1fvnd  11263  shftfvalg  11295  shftfval  11298  caucvgre  11458  rexanuz  11465  recvguniq  11472  rennim  11479  resqrexlemf  11484  rsqrmo  11504  fimaxre2  11704  climeu  11773  sumdc  11835  summodc  11860  zsumdc  11861  isum  11862  fisumss  11869  isumss2  11870  fsumsplit  11884  sumsnf  11886  fsumsplitsn  11887  sumtp  11891  sumsplitdc  11909  fsum2dlemstep  11911  fisum0diag2  11924  fsumconst  11931  modfsummodlemstep  11934  fsum00  11939  fsumabs  11942  fsumiun  11954  isumlessdc  11973  expcnv  11981  prodmodc  12055  zproddc  12056  iprodap  12057  iprodap0  12059  fprodssdc  12067  prodsnf  12069  fprodsplitdc  12073  fprodsplit  12074  fprodm1  12075  fprod1p  12076  fprodunsn  12081  fprod2dlemstep  12099  fprodsplitsn  12110  ef0lem  12137  modmulconst  12300  dvdsdivcl  12327  dvdsssfz1  12329  dvdsfac  12337  zeoxor  12346  nn0ehalf  12380  nn0oddm1d2  12386  nnoddm1d2  12387  divalglemeunn  12398  divalglemeuneg  12400  bitsfzolem  12431  bitsinv1  12439  gcdsupex  12444  gcdsupcl  12445  bezoutlemnewy  12483  bezoutlemmain  12485  bezoutlemeu  12494  dfgcd2  12501  nnwosdc  12526  nninfct  12528  algrf  12533  algcvgblem  12537  lcmgcdlem  12565  lcmdvds  12567  coprmgcdb  12576  mulgcddvds  12582  qredeu  12585  cncongr1  12591  cncongr2  12592  isprm2lem  12604  dvdsnprmd  12613  prmdc  12618  oddprmge3  12623  pw2dvdseu  12656  phibndlem  12704  dfphi2  12708  hashdvds  12709  phiprmpw  12710  eulerthlemh  12719  hashgcdeq  12728  phisum  12729  odzdvds  12734  reumodprminv  12742  nnnn0modprm0  12744  prm23ge5  12753  pclemdc  12777  pcdvdsb  12809  difsqpwdvds  12827  oddprmdvds  12843  1arith  12856  4sqlem3  12879  4sqlemafi  12884  4sqlemffi  12885  4sqleminfi  12886  4sqexercise1  12887  4sqlem11  12890  4sqlem19  12898  ennnfonelemdc  12936  ennnfonelemh  12941  ennnfonelemhf1o  12950  ennnfonelemf1  12955  ennnfonelemrn  12956  ennnfonelemdm  12957  exmidunben  12963  ctinfomlemom  12964  ctinfom  12965  ctiunctlemudc  12974  ctiunctlemf  12975  ctiunctal  12978  nninfdclemcl  12985  nninfdclemf  12986  nninfdclemp1  12987  isstructim  13012  setsresg  13036  strleund  13102  1strbas  13116  2strbasg  13119  2stropg  13120  restsspw  13248  tgval  13261  ptex  13263  imasaddfnlemg  13313  fnpr2o  13338  fnpr2ob  13339  mgmidsssn0  13383  fngsum  13387  igsumvalx  13388  isnsgrp  13405  sgrpidmndm  13419  mndinvmod  13444  mnd1  13454  mhmeql  13491  grpinveu  13537  prdsinvlem  13607  mulgval  13625  subgintm  13701  trivsubgsnd  13704  eqgfval  13725  ecqusaddd  13741  ecqusaddcl  13742  ghmeql  13770  iscmnd  13801  imasabl  13839  gsumfzmhm2  13847  rnglz  13874  srgfcl  13902  reldvdsrsrg  14021  rhmopp  14105  subrgdvds  14164  lssuni  14292  lssintclm  14313  lspf  14318  qusmulrng  14461  mulgrhm2  14539  znf1o  14580  psrbagfi  14602  psr1clfi  14617  mplsubgfilemcl  14628  istopon  14652  toponcom  14666  topgele  14668  topontopn  14676  tsettps  14677  eltg2b  14693  unitg  14701  tgss2  14718  bastop2  14723  distop  14724  epttop  14729  cldss2  14745  neisspw  14787  neipsm  14793  neiuni  14800  tgcn  14847  tgcnp  14848  cnntr  14864  lmff  14888  txuni2  14895  txbasex  14896  txbas  14897  txcnp  14910  txcnmpt  14912  txcn  14914  txdis  14916  txdis1cn  14917  cnmpt11  14922  cnmpt12  14926  cnmpt21  14930  cnmpt2t  14932  cnmpt22  14933  blsscls2  15132  xmetxpbl  15147  xmettxlem  15148  tgqioo  15194  fsumcncntop  15206  cncfmpt1f  15237  mulcncflem  15246  mulcncf  15247  dedekindeu  15262  dedekindicclemicc  15271  dedekindicc  15272  ivthinclemdisj  15279  hovercncf  15285  limcimo  15304  cnmptlimc  15313  reldvg  15318  dvfvalap  15320  dvfgg  15327  dvmptfsum  15364  dveflem  15365  dvef  15366  elply2  15374  sincn  15408  coscn  15409  reeff1o  15412  pilem3  15422  ioocosf1o  15493  mpodvdsmulf1o  15629  fsumdvdsmul  15630  perfectlem2  15639  lgsne0  15682  gausslemma2dlem1a  15702  gausslemma2dlem4  15708  lgseisenlem2  15715  lgseisenlem3  15716  lgsquadlem2  15722  2lgslem3  15745  2sqlem2  15759  mul2sq  15760  2sqlem3  15761  2sqlem7  15765  edgstruct  15829  pw0ss  15848  incistruhgr  15855  upgrex  15868  umgrnloop0  15882  lfgrnloopen  15896  umgredg  15908  umgrnloop2  15914  uspgredgiedg  15941  uspgriedgedg  15942  usgrislfuspgrdom  15953  usgredg3  15977  uspgredg2vlem  15983  uspgredg2v  15984  ushgredgedg  15989  ushgredgedgloop  15991  bj-trst  16013  bj-fast  16015  bj-stand  16022  bj-trdc  16026  bj-fadc  16028  decidr  16070  djulclALT  16075  djurclALT  16076  bj-charfunr  16083  bj-indind  16205  bj-2inf  16211  bj-nntrans2  16225  bj-peano4  16228  bj-nnord  16231  bj-inf2vn  16247  bj-inf2vn2  16248  bj-findis  16252  dom1o  16266  pwf1oexmid  16276  subctctexmid  16277  nnsf  16282  nninfsellemdc  16287  nninffeq  16297  nnnninfen  16298  exmidsbthrlem  16301  sbthom  16305  triap  16308  trilpo  16322  apdifflemr  16326  redcwlpo  16334  tridceq  16335  nconstwlpolem0  16342  nconstwlpolem  16344  nconstwlpo  16345  neapmkv  16347  ltlenmkv  16349