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  mpnanrd  697  oibabs  719  dcim  846  dcstab  849  stdcndc  850  stdcndcOLD  851  dcand  938  dcor  941  dfifp2dc  987  3mix1  1190  3mix2  1191  3jca  1201  syl3anbrc  1205  syl21anbrc  1206  inegd  1414  pclem6  1416  xoranor  1419  dcfrompeirce  1492  nfxfrd  1521  nfd  1569  hban  1593  nfan1  1610  nford  1613  nfand  1614  hbim1  1616  nfal  1622  alexim  1691  nnal  1695  ax6blem  1696  nf4r  1717  19.34  1730  nfexd  1807  sbcof2  1856  nfsb2or  1883  sbidm  1897  nfdv  1923  nfd2  2073  nfeudv  2092  mon  2106  eumo  2109  mo23  2119  eu2  2122  eu3h  2123  exmodc  2128  exmonim  2129  mo2r  2130  mo3h  2131  bm1.1  2214  eqrdv  2227  3eltr4g  2315  abbi2dv  2348  abbi1dv  2349  nfcd  2367  nfcxfrd  2370  dcned  2406  neqned  2407  3netr4g  2435  necon3bi  2450  necon2ai  2454  nnral  2520  alral  2575  rspe  2579  rsp2e  2581  rgen2a  2584  ralrimi  2601  r19.27v  2658  r19.28v  2659  r19.27av  2666  r19.32r  2677  nfreudxy  2705  mormo  2748  nrexrmo  2753  cgsex2g  2836  cgsex4g  2837  spc2egv  2893  spc2gv  2894  spc3egv  2895  spc3gv  2896  rspce  2902  ceqex  2930  elrab3t  2958  elrabd  2961  mosubt  2980  mo2icl  2982  reu3  2993  reu6i  2994  2rmorex  3009  sbc5  3052  rspesbca  3114  rmo2ilem  3119  sbnfc2  3185  ssrd  3229  ssrdv  3230  3sstr4g  3267  eqsstrid  3270  ss2abdv  3297  abssdv  3298  rabssdv  3304  ss2rabdv  3305  ssun1  3367  unssad  3381  unssbd  3382  ssddif  3438  uneqin  3455  indifdir  3460  undif3ss  3465  reuss2  3484  n0rf  3504  reximdva0m  3507  rabxmdc  3523  ssindif0im  3551  minel  3553  ralidm  3592  ralm  3595  dcun  3601  ifmdc  3645  disjsn2  3729  absneu  3738  rabsneu  3739  opprc  3878  elunii  3893  dfnfc2  3906  uniss2  3919  unidif  3920  ssunieq  3921  intab  3952  iunss2  4010  iunssd  4011  iunxdif2  4014  invdisj  4076  disjiun  4078  3brtr4g  4117  trin  4192  triun  4195  truni  4196  trint  4197  iinexgm  4239  class2seteq  4248  pwuni  4277  exmid1dc  4285  exmidn0m  4286  exmidsssn  4287  exmid0el  4289  exmidel  4290  exmidundif  4291  exmidundifim  4292  exmid1stab  4293  mss  4313  copsex2t  4332  euotd  4342  pwunim  4378  ispod  4396  sotricim  4415  exse  4428  frind  4444  trssord  4472  suctr  4513  pwnex  4541  eusvnf  4545  eusvnfb  4546  eusv2nf  4548  rexxfrd  4555  ralxfr2d  4556  rexxfr2d  4557  rabxfrd  4561  reuhypd  4563  eldifpw  4569  iunpw  4572  ssorduni  4580  onsucb  4596  onsucelsucr  4601  sucunielr  4603  ontriexmidim  4615  ordtri2or2exmidlem  4619  onsucelsucexmid  4623  reg2exmidlema  4627  setindel  4631  elirr  4634  orddisj  4639  en2lp  4647  suc11g  4650  ordsuc  4656  nlimsucg  4659  ordtri2or2exmid  4664  ontri2orexmidim  4665  zfregfr  4667  wessep  4671  tfi  4675  peano5  4691  limom  4707  peano2b  4708  nndceq0  4711  nnpredcl  4716  0nelrel  4767  eqrelrdv  4817  xpsspw  4833  relint  4846  relop  4875  eqbrrdva  4895  ssrelrn  4917  opeldm  4929  reldmm  4945  elres  5044  relssres  5046  elrelimasn  5097  exse2  5105  issref  5114  trin2  5123  dminss  5146  imainss  5147  rnxpid  5166  dmsn0el  5201  dmmptg  5229  relrelss  5258  cnviinm  5273  iotanul  5297  sniota  5312  dffun5r  5333  funmo  5336  funco  5361  funun  5365  fununmo  5366  fununfun  5367  funprg  5374  funtpg  5375  funtp  5377  fntpg  5380  fununi  5392  funcnvuni  5393  imadiflem  5403  imainlem  5405  funimaexglem  5407  isarep2  5411  fnunsn  5433  2elresin  5437  fnimadisj  5447  dmmptd  5457  fco  5494  funssxp  5498  fssres  5506  feu  5513  fimacnvdisj  5515  fabexg  5518  f00  5522  f0rn0  5525  f1co  5548  fores  5563  foco  5564  f1ores  5592  foimacnv  5595  f1oun  5597  fun11iun  5598  f1oco  5600  fo00  5614  brprcneu  5625  fv3  5655  relelfvdm  5664  nfvres  5668  nfunsn  5669  funfvbrb  5753  respreima  5768  dff2  5784  dff3im  5785  dffo4  5788  fvmptelcdm  5793  ffvresb  5803  f1oresrab  5805  fmptco  5806  fsn  5812  fcof  5825  fpr  5828  ftpg  5830  fsnunf  5846  fsnunfv  5847  elabrex  5890  dff1o6  5909  foeqcnvco  5923  fliftel1  5927  isores1  5947  isoini2  5952  riotasbc  5980  acexmidlemph  6003  acexmidlemcase  6005  oprabidlem  6041  brabvv  6059  eloprabga  6100  fnoprabg  6114  caovimo  6208  oprabexd  6281  uchoice  6292  fo1stresm  6316  fo2ndresm  6317  unielxp  6329  1st2ndbr  6339  opabn1stprc  6350  fmpoco  6373  1stconst  6378  2ndconst  6379  poxp  6389  spc2ed  6390  disjxp1  6393  reldmtpos  6410  tposfun  6417  dftpos4  6420  smores  6449  smores2  6451  tfrlem1  6465  tfr0dm  6479  tfrlemibxssdm  6484  tfrlemibex  6486  tfrlemiubacc  6487  tfrlemi14d  6490  tfrexlem  6491  tfri1d  6492  tfr1onlembxssdm  6500  tfr1onlembex  6502  tfr1onlemubacc  6503  tfr1onlemres  6506  tfrcllemsucfn  6510  tfrcllembxssdm  6513  tfrcllembex  6515  tfrcllemubacc  6516  tfrcllemres  6519  tfri3  6524  rdgon  6543  frecabcl  6556  frecfcllem  6561  frecrdg  6565  2oconcl  6598  nnsucelsuc  6650  nntri3or  6652  nndceq  6658  nndcel  6659  dcdifsnid  6663  ecexr  6698  brdifun  6720  ecelqsdm  6765  iinerm  6767  eroveu  6786  erovlem  6787  ecopovtrn  6792  ecopovtrng  6795  th3qlem1  6797  pmsspw  6843  map0b  6847  mapsn  6850  mapsncnv  6855  ixpf  6880  uniixp  6881  ixpexgg  6882  resixp  6893  f1oen3g  6918  ssdomg  6943  domtr  6950  snfig  6980  enpr2d  6985  dom1o  6990  xpf1o  7018  xpmapenlem  7023  php5dom  7037  fidceq  7044  nnfi  7047  fiunsnnn  7056  findcard  7063  findcard2  7064  findcard2s  7065  ac6sfi  7073  fidcen  7074  tridc  7075  fimax2gtri  7077  finexdc  7078  elssdc  7080  eqsndc  7081  exmidpw  7086  exmidpweq  7087  exmidpw2en  7090  nnwetri  7094  unsnfi  7097  unsnfidcex  7098  unsnfidcel  7099  undifdcss  7101  tpfidisj  7107  tpfidceq  7108  iunfidisj  7129  snexxph  7133  fidcenumlemrks  7136  sbthlem2  7141  sbthlemi3  7142  sbthlem7  7146  sbthlemi8  7147  fival  7153  dcfi  7164  supmoti  7176  djuss  7253  updjudhf  7262  updjud  7265  casefun  7268  caseinj  7272  omp1eomlem  7277  djufun  7287  djuinj  7289  ctssdccl  7294  ctfoex  7301  nnnninf  7309  nnnninfeq2  7312  nninfisollem0  7313  nninfisollemne  7314  nninfisollemeq  7315  nninfisol  7316  finomni  7323  exmidomniim  7324  exmidomni  7325  fodjuomnilemdc  7327  omniwomnimkv  7350  nninfdcinf  7354  nninfwlporlem  7356  nninfwlpoimlemg  7358  nninfwlpoim  7362  nninfinfwlpo  7363  exmidonfinlem  7387  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  finacn  7402  exmidaclem  7406  dju1en  7411  exmidontriimlem1  7419  exmidontriimlem3  7421  iftrueb01  7424  pw1on  7427  3nsssucpw1  7437  2omotaplemap  7459  2omotap  7461  exmidmotap  7463  cc4f  7471  cc4n  7473  acnccim  7474  dmaddpqlem  7580  nqpi  7581  dmaddpq  7582  dmmulpq  7583  ltdcnq  7600  subhalfnqq  7617  enq0sym  7635  enq0ref  7636  enq0tr  7637  nqnq0pi  7641  nq0nn  7645  addnq0mo  7650  mulnq0mo  7651  nqpnq0nq  7656  nqnq0a  7657  nqnq0m  7658  npsspw  7674  elnp1st2nd  7679  prnmaxl  7691  prnminu  7692  prarloc  7706  genprndl  7724  genprndu  7725  nqprm  7745  nqprl  7754  nqpru  7755  addnqprlemrl  7760  addnqprlemru  7761  prmuloc  7769  mulnqprlemrl  7776  mulnqprlemru  7777  ltsopr  7799  ltexprlemm  7803  ltexprlemopl  7804  ltexprlemopu  7806  lteupri  7820  recexprlemopl  7828  recexprlemopu  7830  recexprlemdisj  7833  archpr  7846  cauappcvgprlemdisj  7854  cauappcvgprlemladdrl  7860  cauappcvgprlem2  7863  caucvgprlemnbj  7870  caucvgprlemdisj  7877  caucvgprlemladdfu  7880  caucvgprlem2  7883  caucvgprprlemnbj  7896  caucvgprprlemdisj  7905  suplocexprlemml  7919  suplocexprlemrl  7920  suplocexprlemmu  7921  suplocexprlemloc  7924  addsrmo  7946  mulsrmo  7947  recexgt0sr  7976  prsrpos  7988  caucvgsrlemasr  7993  suplocsrlemb  8009  suplocsrlempr  8010  suplocsr  8012  elrealeu  8032  pitonn  8051  pitoregt0  8052  pitore  8053  recnnre  8054  axaddcl  8067  axaddrcl  8068  axmulcl  8069  axmulrcl  8070  axrnegex  8082  axcnre  8084  axpre-lttrn  8087  rereceu  8092  axarch  8094  axpre-suploclemres  8104  axpre-suploc  8105  ltxrlt  8228  apirr  8768  divmulasscomap  8859  rerecclap  8893  lbreu  9108  arch  9382  0mnnnnn0  9417  nnm1nn0  9426  elnnnn0c  9430  elnnz1  9485  ztri3or0  9504  nzadd  9515  nn0n0n1ge2  9533  zdceq  9538  zdcle  9539  zdclt  9540  uzind  9574  eluzge3nn  9784  supinfneg  9807  infsupneg  9808  eluz2b2  9815  elnn1uz2  9819  elnn0dc  9823  elnndc  9824  nn01to3  9829  znq  9836  qaddcl  9847  qmulcl  9849  qreccl  9854  irradd  9858  irrmul  9859  elpq  9861  cnref1o  9863  xnn0dcle  10015  xrpnfdc  10055  xrmnfdc  10056  xaddcom  10074  xnegdi  10081  xpncan  10084  xleadd1a  10086  iooidg  10122  elioo4g  10147  elfzd  10229  fzdcel  10253  fznlem  10254  fzpreddisj  10284  fz0to4untppr  10337  elfz0ubfz0  10338  elfz0fzfz0  10339  fz0fzelfz0  10340  fz0fzdiffz0  10343  elfzmlbp  10345  difelfzle  10347  4fvwrd4  10353  fzosplit  10392  elfzo0  10399  fzo1fzo0n0  10400  elfzonn0  10403  fzofzim  10405  elfzo1  10408  elfzom1elp1fzo  10425  fzossfzop1  10435  ssfzo12bi  10448  exfzdc  10463  zsupcllemstep  10466  infssuzex  10470  qdceq  10481  qdclt  10482  exbtwnzlemstep  10484  exbtwnzlemex  10486  exbtwnz  10487  rebtwn2zlemstep  10489  rebtwn2z  10491  qbtwnxr  10494  modfzo0difsn  10634  frec2uzrand  10644  frec2uzf1od  10645  frecuzrdgrcl  10649  frecuzrdgtcl  10651  frecuzrdgrclt  10654  frecuzrdgfunlem  10658  frecfzennn  10665  nninfinf  10682  seq3f1olemp  10754  seq3f1oleml  10755  seqf1oglem1  10758  ser0f  10773  expcl2lemap  10790  hashunsng  11047  iswrdinn0  11094  snopiswrd  11099  wrdlndm  11106  iswrdsymb  11107  wrdsymb1  11126  ccatfv0  11156  ccatval21sw  11158  lswccatn0lsw  11164  eqs1  11181  ccat1st1st  11193  lswccats1fst  11196  fzowrddc  11200  swrdfv0  11207  swrdlen2  11215  swrdfv2  11216  swrdsbslen  11219  swrdspsleq  11220  pfxfv0  11245  pfxtrcfv0  11247  pfxeq  11249  pfx1  11256  swrdswrdlem  11257  cats1un  11274  pfxccatin12lem2a  11280  pfxccatin12lem2  11284  pfxccatin12lem3  11285  swrdccat  11288  cats1fvn  11317  cats1fvnd  11318  shftfvalg  11350  shftfval  11353  caucvgre  11513  rexanuz  11520  recvguniq  11527  rennim  11534  resqrexlemf  11539  rsqrmo  11559  fimaxre2  11759  climeu  11828  sumdc  11890  summodc  11915  zsumdc  11916  isum  11917  fisumss  11924  isumss2  11925  fsumsplit  11939  sumsnf  11941  fsumsplitsn  11942  sumtp  11946  sumsplitdc  11964  fsum2dlemstep  11966  fisum0diag2  11979  fsumconst  11986  modfsummodlemstep  11989  fsum00  11994  fsumabs  11997  fsumiun  12009  isumlessdc  12028  expcnv  12036  prodmodc  12110  zproddc  12111  iprodap  12112  iprodap0  12114  fprodssdc  12122  prodsnf  12124  fprodsplitdc  12128  fprodsplit  12129  fprodm1  12130  fprod1p  12131  fprodunsn  12136  fprod2dlemstep  12154  fprodsplitsn  12165  ef0lem  12192  modmulconst  12355  dvdsdivcl  12382  dvdsssfz1  12384  dvdsfac  12392  zeoxor  12401  nn0ehalf  12435  nn0oddm1d2  12441  nnoddm1d2  12442  divalglemeunn  12453  divalglemeuneg  12455  bitsfzolem  12486  bitsinv1  12494  gcdsupex  12499  gcdsupcl  12500  bezoutlemnewy  12538  bezoutlemmain  12540  bezoutlemeu  12549  dfgcd2  12556  nnwosdc  12581  nninfct  12583  algrf  12588  algcvgblem  12592  lcmgcdlem  12620  lcmdvds  12622  coprmgcdb  12631  mulgcddvds  12637  qredeu  12640  cncongr1  12646  cncongr2  12647  isprm2lem  12659  dvdsnprmd  12668  prmdc  12673  oddprmge3  12678  pw2dvdseu  12711  phibndlem  12759  dfphi2  12763  hashdvds  12764  phiprmpw  12765  eulerthlemh  12774  hashgcdeq  12783  phisum  12784  odzdvds  12789  reumodprminv  12797  nnnn0modprm0  12799  prm23ge5  12808  pclemdc  12832  pcdvdsb  12864  difsqpwdvds  12882  oddprmdvds  12898  1arith  12911  4sqlem3  12934  4sqlemafi  12939  4sqlemffi  12940  4sqleminfi  12941  4sqexercise1  12942  4sqlem11  12945  4sqlem19  12953  ennnfonelemdc  12991  ennnfonelemh  12996  ennnfonelemhf1o  13005  ennnfonelemf1  13010  ennnfonelemrn  13011  ennnfonelemdm  13012  exmidunben  13018  ctinfomlemom  13019  ctinfom  13020  ctiunctlemudc  13029  ctiunctlemf  13030  ctiunctal  13033  nninfdclemcl  13040  nninfdclemf  13041  nninfdclemp1  13042  isstructim  13067  setsresg  13091  strleund  13157  1strbas  13171  2strbasg  13174  2stropg  13175  restsspw  13303  tgval  13316  ptex  13318  imasaddfnlemg  13368  fnpr2o  13393  fnpr2ob  13394  mgmidsssn0  13438  fngsum  13442  igsumvalx  13443  isnsgrp  13460  sgrpidmndm  13474  mndinvmod  13499  mnd1  13509  mhmeql  13546  grpinveu  13592  prdsinvlem  13662  mulgval  13680  subgintm  13756  trivsubgsnd  13759  eqgfval  13780  ecqusaddd  13796  ecqusaddcl  13797  ghmeql  13825  iscmnd  13856  imasabl  13894  gsumfzmhm2  13902  rnglz  13929  srgfcl  13957  rhmopp  14161  subrgdvds  14220  lssuni  14348  lssintclm  14369  lspf  14374  qusmulrng  14517  mulgrhm2  14595  znf1o  14636  psrbagfi  14658  psr1clfi  14673  mplsubgfilemcl  14684  istopon  14708  toponcom  14722  topgele  14724  topontopn  14732  tsettps  14733  eltg2b  14749  unitg  14757  tgss2  14774  bastop2  14779  distop  14780  epttop  14785  cldss2  14801  neisspw  14843  neipsm  14849  neiuni  14856  tgcn  14903  tgcnp  14904  cnntr  14920  lmff  14944  txuni2  14951  txbasex  14952  txbas  14953  txcnp  14966  txcnmpt  14968  txcn  14970  txdis  14972  txdis1cn  14973  cnmpt11  14978  cnmpt12  14982  cnmpt21  14986  cnmpt2t  14988  cnmpt22  14989  blsscls2  15188  xmetxpbl  15203  xmettxlem  15204  tgqioo  15250  fsumcncntop  15262  cncfmpt1f  15293  mulcncflem  15302  mulcncf  15303  dedekindeu  15318  dedekindicclemicc  15327  dedekindicc  15328  ivthinclemdisj  15335  hovercncf  15341  limcimo  15360  cnmptlimc  15369  reldvg  15374  dvfvalap  15376  dvfgg  15383  dvmptfsum  15420  dveflem  15421  dvef  15422  elply2  15430  sincn  15464  coscn  15465  reeff1o  15468  pilem3  15478  ioocosf1o  15549  mpodvdsmulf1o  15685  fsumdvdsmul  15686  perfectlem2  15695  lgsne0  15738  gausslemma2dlem1a  15758  gausslemma2dlem4  15764  lgseisenlem2  15771  lgseisenlem3  15772  lgsquadlem2  15778  2lgslem3  15801  2sqlem2  15815  mul2sq  15816  2sqlem3  15817  2sqlem7  15821  edgstruct  15885  pw0ss  15904  incistruhgr  15911  upgrex  15924  umgrnloop0  15938  lfgrnloopen  15952  umgredg  15964  umgrnloop2  15970  uspgredgiedg  15997  uspgriedgedg  15998  usgrislfuspgrdom  16009  usgredg3  16033  uspgredg2vlem  16039  uspgredg2v  16040  ushgredgedg  16045  ushgredgedgloop  16047  uhgr0vsize0en  16054  usgr1e  16060  vtxedgfi  16075  vtxlpfi  16076  vtxdumgrfival  16084  wlkcprim  16122  wlk1walkdom  16131  uspgr2wlkeq  16137  upgr2wlkdc  16147  wlkres  16149  clwwlkccatlem  16169  clwwlknp  16185  umgr2cwwk2dif  16192  bj-trst  16212  bj-fast  16214  bj-stand  16221  bj-trdc  16225  bj-fadc  16227  decidr  16269  djulclALT  16274  djurclALT  16275  bj-charfunr  16282  bj-indind  16404  bj-2inf  16410  bj-nntrans2  16424  bj-peano4  16427  bj-nnord  16430  bj-inf2vn  16446  bj-inf2vn2  16447  bj-findis  16451  pwf1oexmid  16478  subctctexmid  16479  pw1dceq  16483  nnsf  16485  nninfsellemdc  16490  nninffeq  16500  nnnninfen  16501  exmidsbthrlem  16504  sbthom  16508  triap  16511  trilpo  16525  apdifflemr  16529  redcwlpo  16537  tridceq  16538  nconstwlpolem0  16545  nconstwlpolem  16547  nconstwlpo  16548  neapmkv  16550  ltlenmkv  16552