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  4238  class2seteq  4247  pwuni  4276  exmid1dc  4284  exmidn0m  4285  exmidsssn  4286  exmid0el  4288  exmidel  4289  exmidundif  4290  exmidundifim  4291  exmid1stab  4292  mss  4312  copsex2t  4331  euotd  4341  pwunim  4377  ispod  4395  sotricim  4414  exse  4427  frind  4443  trssord  4471  suctr  4512  pwnex  4540  eusvnf  4544  eusvnfb  4545  eusv2nf  4547  rexxfrd  4554  ralxfr2d  4555  rexxfr2d  4556  rabxfrd  4560  reuhypd  4562  eldifpw  4568  iunpw  4571  ssorduni  4579  onsucb  4595  onsucelsucr  4600  sucunielr  4602  ontriexmidim  4614  ordtri2or2exmidlem  4618  onsucelsucexmid  4622  reg2exmidlema  4626  setindel  4630  elirr  4633  orddisj  4638  en2lp  4646  suc11g  4649  ordsuc  4655  nlimsucg  4658  ordtri2or2exmid  4663  ontri2orexmidim  4664  zfregfr  4666  wessep  4670  tfi  4674  peano5  4690  limom  4706  peano2b  4707  nndceq0  4710  nnpredcl  4715  0nelrel  4765  eqrelrdv  4815  xpsspw  4831  relint  4843  relop  4872  eqbrrdva  4892  ssrelrn  4914  opeldm  4926  reldmm  4942  elres  5041  relssres  5043  elrelimasn  5094  exse2  5102  issref  5111  trin2  5120  dminss  5143  imainss  5144  rnxpid  5163  dmsn0el  5198  dmmptg  5226  relrelss  5255  cnviinm  5270  iotanul  5294  sniota  5309  dffun5r  5330  funmo  5333  funco  5358  funun  5362  fununmo  5363  fununfun  5364  funprg  5371  funtpg  5372  funtp  5374  fntpg  5377  fununi  5389  funcnvuni  5390  imadiflem  5400  imainlem  5402  funimaexglem  5404  isarep2  5408  fnunsn  5430  2elresin  5434  fnimadisj  5444  dmmptd  5454  fco  5491  funssxp  5495  fssres  5503  feu  5510  fimacnvdisj  5512  fabexg  5515  f00  5519  f0rn0  5522  f1co  5545  fores  5560  foco  5561  f1ores  5589  foimacnv  5592  f1oun  5594  fun11iun  5595  f1oco  5597  fo00  5611  brprcneu  5622  fv3  5652  relelfvdm  5661  nfvres  5665  nfunsn  5666  funfvbrb  5750  respreima  5765  dff2  5781  dff3im  5782  dffo4  5785  fvmptelcdm  5790  ffvresb  5800  f1oresrab  5802  fmptco  5803  fsn  5809  fcof  5822  fpr  5825  ftpg  5827  fsnunf  5843  fsnunfv  5844  elabrex  5887  dff1o6  5906  foeqcnvco  5920  fliftel1  5924  isores1  5944  isoini2  5949  riotasbc  5977  acexmidlemph  6000  acexmidlemcase  6002  oprabidlem  6038  brabvv  6056  eloprabga  6097  fnoprabg  6111  caovimo  6205  oprabexd  6278  uchoice  6289  fo1stresm  6313  fo2ndresm  6314  unielxp  6326  1st2ndbr  6336  fmpoco  6368  1stconst  6373  2ndconst  6374  poxp  6384  spc2ed  6385  disjxp1  6388  reldmtpos  6405  tposfun  6412  dftpos4  6415  smores  6444  smores2  6446  tfrlem1  6460  tfr0dm  6474  tfrlemibxssdm  6479  tfrlemibex  6481  tfrlemiubacc  6482  tfrlemi14d  6485  tfrexlem  6486  tfri1d  6487  tfr1onlembxssdm  6495  tfr1onlembex  6497  tfr1onlemubacc  6498  tfr1onlemres  6501  tfrcllemsucfn  6505  tfrcllembxssdm  6508  tfrcllembex  6510  tfrcllemubacc  6511  tfrcllemres  6514  tfri3  6519  rdgon  6538  frecabcl  6551  frecfcllem  6556  frecrdg  6560  2oconcl  6593  nnsucelsuc  6645  nntri3or  6647  nndceq  6653  nndcel  6654  dcdifsnid  6658  ecexr  6693  brdifun  6715  ecelqsdm  6760  iinerm  6762  eroveu  6781  erovlem  6782  ecopovtrn  6787  ecopovtrng  6790  th3qlem1  6792  pmsspw  6838  map0b  6842  mapsn  6845  mapsncnv  6850  ixpf  6875  uniixp  6876  ixpexgg  6877  resixp  6888  f1oen3g  6913  ssdomg  6938  domtr  6945  snfig  6975  enpr2d  6980  dom1o  6985  xpf1o  7013  xpmapenlem  7018  php5dom  7032  fidceq  7039  nnfi  7042  fiunsnnn  7051  findcard  7058  findcard2  7059  findcard2s  7060  ac6sfi  7068  tridc  7069  fimax2gtri  7071  finexdc  7072  exmidpw  7078  exmidpweq  7079  exmidpw2en  7082  nnwetri  7086  unsnfi  7089  unsnfidcex  7090  unsnfidcel  7091  undifdcss  7093  tpfidisj  7099  tpfidceq  7100  iunfidisj  7121  snexxph  7125  fidcenumlemrks  7128  sbthlem2  7133  sbthlemi3  7134  sbthlem7  7138  sbthlemi8  7139  fival  7145  dcfi  7156  supmoti  7168  djuss  7245  updjudhf  7254  updjud  7257  casefun  7260  caseinj  7264  omp1eomlem  7269  djufun  7279  djuinj  7281  ctssdccl  7286  ctfoex  7293  nnnninf  7301  nnnninfeq2  7304  nninfisollem0  7305  nninfisollemne  7306  nninfisollemeq  7307  nninfisol  7308  finomni  7315  exmidomniim  7316  exmidomni  7317  fodjuomnilemdc  7319  omniwomnimkv  7342  nninfdcinf  7346  nninfwlporlem  7348  nninfwlpoimlemg  7350  nninfwlpoim  7354  nninfinfwlpo  7355  exmidonfinlem  7379  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  finacn  7394  exmidaclem  7398  dju1en  7403  exmidontriimlem1  7411  exmidontriimlem3  7413  iftrueb01  7416  pw1on  7419  3nsssucpw1  7429  2omotaplemap  7451  2omotap  7453  exmidmotap  7455  cc4f  7463  cc4n  7465  acnccim  7466  dmaddpqlem  7572  nqpi  7573  dmaddpq  7574  dmmulpq  7575  ltdcnq  7592  subhalfnqq  7609  enq0sym  7627  enq0ref  7628  enq0tr  7629  nqnq0pi  7633  nq0nn  7637  addnq0mo  7642  mulnq0mo  7643  nqpnq0nq  7648  nqnq0a  7649  nqnq0m  7650  npsspw  7666  elnp1st2nd  7671  prnmaxl  7683  prnminu  7684  prarloc  7698  genprndl  7716  genprndu  7717  nqprm  7737  nqprl  7746  nqpru  7747  addnqprlemrl  7752  addnqprlemru  7753  prmuloc  7761  mulnqprlemrl  7768  mulnqprlemru  7769  ltsopr  7791  ltexprlemm  7795  ltexprlemopl  7796  ltexprlemopu  7798  lteupri  7812  recexprlemopl  7820  recexprlemopu  7822  recexprlemdisj  7825  archpr  7838  cauappcvgprlemdisj  7846  cauappcvgprlemladdrl  7852  cauappcvgprlem2  7855  caucvgprlemnbj  7862  caucvgprlemdisj  7869  caucvgprlemladdfu  7872  caucvgprlem2  7875  caucvgprprlemnbj  7888  caucvgprprlemdisj  7897  suplocexprlemml  7911  suplocexprlemrl  7912  suplocexprlemmu  7913  suplocexprlemloc  7916  addsrmo  7938  mulsrmo  7939  recexgt0sr  7968  prsrpos  7980  caucvgsrlemasr  7985  suplocsrlemb  8001  suplocsrlempr  8002  suplocsr  8004  elrealeu  8024  pitonn  8043  pitoregt0  8044  pitore  8045  recnnre  8046  axaddcl  8059  axaddrcl  8060  axmulcl  8061  axmulrcl  8062  axrnegex  8074  axcnre  8076  axpre-lttrn  8079  rereceu  8084  axarch  8086  axpre-suploclemres  8096  axpre-suploc  8097  ltxrlt  8220  apirr  8760  divmulasscomap  8851  rerecclap  8885  lbreu  9100  arch  9374  0mnnnnn0  9409  nnm1nn0  9418  elnnnn0c  9422  elnnz1  9477  ztri3or0  9496  nzadd  9507  nn0n0n1ge2  9525  zdceq  9530  zdcle  9531  zdclt  9532  uzind  9566  eluzge3nn  9775  supinfneg  9798  infsupneg  9799  eluz2b2  9806  elnn1uz2  9810  elnn0dc  9814  elnndc  9815  nn01to3  9820  znq  9827  qaddcl  9838  qmulcl  9840  qreccl  9845  irradd  9849  irrmul  9850  elpq  9852  cnref1o  9854  xnn0dcle  10006  xrpnfdc  10046  xrmnfdc  10047  xaddcom  10065  xnegdi  10072  xpncan  10075  xleadd1a  10077  iooidg  10113  elioo4g  10138  elfzd  10220  fzdcel  10244  fznlem  10245  fzpreddisj  10275  fz0to4untppr  10328  elfz0ubfz0  10329  elfz0fzfz0  10330  fz0fzelfz0  10331  fz0fzdiffz0  10334  elfzmlbp  10336  difelfzle  10338  4fvwrd4  10344  fzosplit  10383  elfzo0  10390  fzo1fzo0n0  10391  elfzonn0  10394  fzofzim  10396  elfzo1  10399  elfzom1elp1fzo  10416  fzossfzop1  10426  ssfzo12bi  10439  exfzdc  10454  zsupcllemstep  10457  infssuzex  10461  qdceq  10472  qdclt  10473  exbtwnzlemstep  10475  exbtwnzlemex  10477  exbtwnz  10478  rebtwn2zlemstep  10480  rebtwn2z  10482  qbtwnxr  10485  modfzo0difsn  10625  frec2uzrand  10635  frec2uzf1od  10636  frecuzrdgrcl  10640  frecuzrdgtcl  10642  frecuzrdgrclt  10645  frecuzrdgfunlem  10649  frecfzennn  10656  nninfinf  10673  seq3f1olemp  10745  seq3f1oleml  10746  seqf1oglem1  10749  ser0f  10764  expcl2lemap  10781  hashunsng  11037  iswrdinn0  11084  snopiswrd  11089  wrdlndm  11096  iswrdsymb  11097  wrdsymb1  11116  ccatfv0  11146  ccatval21sw  11148  lswccatn0lsw  11154  eqs1  11169  ccat1st1st  11180  lswccats1fst  11183  fzowrddc  11187  swrdfv0  11194  swrdlen2  11202  swrdfv2  11203  swrdsbslen  11206  swrdspsleq  11207  pfxfv0  11232  pfxtrcfv0  11234  pfxeq  11236  pfx1  11243  swrdswrdlem  11244  cats1un  11261  pfxccatin12lem2a  11267  pfxccatin12lem2  11271  pfxccatin12lem3  11272  swrdccat  11275  cats1fvn  11304  cats1fvnd  11305  shftfvalg  11337  shftfval  11340  caucvgre  11500  rexanuz  11507  recvguniq  11514  rennim  11521  resqrexlemf  11526  rsqrmo  11546  fimaxre2  11746  climeu  11815  sumdc  11877  summodc  11902  zsumdc  11903  isum  11904  fisumss  11911  isumss2  11912  fsumsplit  11926  sumsnf  11928  fsumsplitsn  11929  sumtp  11933  sumsplitdc  11951  fsum2dlemstep  11953  fisum0diag2  11966  fsumconst  11973  modfsummodlemstep  11976  fsum00  11981  fsumabs  11984  fsumiun  11996  isumlessdc  12015  expcnv  12023  prodmodc  12097  zproddc  12098  iprodap  12099  iprodap0  12101  fprodssdc  12109  prodsnf  12111  fprodsplitdc  12115  fprodsplit  12116  fprodm1  12117  fprod1p  12118  fprodunsn  12123  fprod2dlemstep  12141  fprodsplitsn  12152  ef0lem  12179  modmulconst  12342  dvdsdivcl  12369  dvdsssfz1  12371  dvdsfac  12379  zeoxor  12388  nn0ehalf  12422  nn0oddm1d2  12428  nnoddm1d2  12429  divalglemeunn  12440  divalglemeuneg  12442  bitsfzolem  12473  bitsinv1  12481  gcdsupex  12486  gcdsupcl  12487  bezoutlemnewy  12525  bezoutlemmain  12527  bezoutlemeu  12536  dfgcd2  12543  nnwosdc  12568  nninfct  12570  algrf  12575  algcvgblem  12579  lcmgcdlem  12607  lcmdvds  12609  coprmgcdb  12618  mulgcddvds  12624  qredeu  12627  cncongr1  12633  cncongr2  12634  isprm2lem  12646  dvdsnprmd  12655  prmdc  12660  oddprmge3  12665  pw2dvdseu  12698  phibndlem  12746  dfphi2  12750  hashdvds  12751  phiprmpw  12752  eulerthlemh  12761  hashgcdeq  12770  phisum  12771  odzdvds  12776  reumodprminv  12784  nnnn0modprm0  12786  prm23ge5  12795  pclemdc  12819  pcdvdsb  12851  difsqpwdvds  12869  oddprmdvds  12885  1arith  12898  4sqlem3  12921  4sqlemafi  12926  4sqlemffi  12927  4sqleminfi  12928  4sqexercise1  12929  4sqlem11  12932  4sqlem19  12940  ennnfonelemdc  12978  ennnfonelemh  12983  ennnfonelemhf1o  12992  ennnfonelemf1  12997  ennnfonelemrn  12998  ennnfonelemdm  12999  exmidunben  13005  ctinfomlemom  13006  ctinfom  13007  ctiunctlemudc  13016  ctiunctlemf  13017  ctiunctal  13020  nninfdclemcl  13027  nninfdclemf  13028  nninfdclemp1  13029  isstructim  13054  setsresg  13078  strleund  13144  1strbas  13158  2strbasg  13161  2stropg  13162  restsspw  13290  tgval  13303  ptex  13305  imasaddfnlemg  13355  fnpr2o  13380  fnpr2ob  13381  mgmidsssn0  13425  fngsum  13429  igsumvalx  13430  isnsgrp  13447  sgrpidmndm  13461  mndinvmod  13486  mnd1  13496  mhmeql  13533  grpinveu  13579  prdsinvlem  13649  mulgval  13667  subgintm  13743  trivsubgsnd  13746  eqgfval  13767  ecqusaddd  13783  ecqusaddcl  13784  ghmeql  13812  iscmnd  13843  imasabl  13881  gsumfzmhm2  13889  rnglz  13916  srgfcl  13944  rhmopp  14148  subrgdvds  14207  lssuni  14335  lssintclm  14356  lspf  14361  qusmulrng  14504  mulgrhm2  14582  znf1o  14623  psrbagfi  14645  psr1clfi  14660  mplsubgfilemcl  14671  istopon  14695  toponcom  14709  topgele  14711  topontopn  14719  tsettps  14720  eltg2b  14736  unitg  14744  tgss2  14761  bastop2  14766  distop  14767  epttop  14772  cldss2  14788  neisspw  14830  neipsm  14836  neiuni  14843  tgcn  14890  tgcnp  14891  cnntr  14907  lmff  14931  txuni2  14938  txbasex  14939  txbas  14940  txcnp  14953  txcnmpt  14955  txcn  14957  txdis  14959  txdis1cn  14960  cnmpt11  14965  cnmpt12  14969  cnmpt21  14973  cnmpt2t  14975  cnmpt22  14976  blsscls2  15175  xmetxpbl  15190  xmettxlem  15191  tgqioo  15237  fsumcncntop  15249  cncfmpt1f  15280  mulcncflem  15289  mulcncf  15290  dedekindeu  15305  dedekindicclemicc  15314  dedekindicc  15315  ivthinclemdisj  15322  hovercncf  15328  limcimo  15347  cnmptlimc  15356  reldvg  15361  dvfvalap  15363  dvfgg  15370  dvmptfsum  15407  dveflem  15408  dvef  15409  elply2  15417  sincn  15451  coscn  15452  reeff1o  15455  pilem3  15465  ioocosf1o  15536  mpodvdsmulf1o  15672  fsumdvdsmul  15673  perfectlem2  15682  lgsne0  15725  gausslemma2dlem1a  15745  gausslemma2dlem4  15751  lgseisenlem2  15758  lgseisenlem3  15759  lgsquadlem2  15765  2lgslem3  15788  2sqlem2  15802  mul2sq  15803  2sqlem3  15804  2sqlem7  15808  edgstruct  15872  pw0ss  15891  incistruhgr  15898  upgrex  15911  umgrnloop0  15925  lfgrnloopen  15939  umgredg  15951  umgrnloop2  15957  uspgredgiedg  15984  uspgriedgedg  15985  usgrislfuspgrdom  15996  usgredg3  16020  uspgredg2vlem  16026  uspgredg2v  16027  ushgredgedg  16032  ushgredgedgloop  16034  wlkcprim  16071  wlk1walkdom  16080  uspgr2wlkeq  16086  upgr2wlkdc  16096  wlkres  16098  bj-trst  16127  bj-fast  16129  bj-stand  16136  bj-trdc  16140  bj-fadc  16142  decidr  16184  djulclALT  16189  djurclALT  16190  bj-charfunr  16197  bj-indind  16319  bj-2inf  16325  bj-nntrans2  16339  bj-peano4  16342  bj-nnord  16345  bj-inf2vn  16361  bj-inf2vn2  16362  bj-findis  16366  fidcen  16379  pwf1oexmid  16394  subctctexmid  16395  pw1dceq  16399  nnsf  16401  nninfsellemdc  16406  nninffeq  16416  nnnninfen  16417  exmidsbthrlem  16420  sbthom  16424  triap  16427  trilpo  16441  apdifflemr  16445  redcwlpo  16453  tridceq  16454  nconstwlpolem0  16461  nconstwlpolem  16463  nconstwlpo  16464  neapmkv  16466  ltlenmkv  16468