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  2837  cgsex4g  2838  spc2egv  2894  spc2gv  2895  spc3egv  2896  spc3gv  2897  rspce  2903  ceqex  2931  elrab3t  2959  elrabd  2962  mosubt  2981  mo2icl  2983  reu3  2994  reu6i  2995  2rmorex  3010  sbc5  3053  rspesbca  3115  rmo2ilem  3120  sbnfc2  3186  ssrd  3230  ssrdv  3231  3sstr4g  3268  eqsstrid  3271  ss2abdv  3298  abssdv  3299  rabssdv  3305  ss2rabdv  3306  ssun1  3368  unssad  3382  unssbd  3383  ssddif  3439  uneqin  3456  indifdir  3461  undif3ss  3466  reuss2  3485  n0rf  3505  reximdva0m  3508  rabxmdc  3524  ssindif0im  3552  minel  3554  ralidm  3593  ralm  3596  dcun  3602  ifmdc  3646  disjsn2  3730  absneu  3739  rabsneu  3740  opprc  3879  elunii  3894  dfnfc2  3907  uniss2  3920  unidif  3921  ssunieq  3922  intab  3953  iunss2  4011  iunssd  4012  iunxdif2  4015  invdisj  4077  disjiun  4079  3brtr4g  4118  trin  4193  triun  4196  truni  4197  trint  4198  iinexgm  4240  class2seteq  4249  pwuni  4278  exmid1dc  4286  exmidn0m  4287  exmidsssn  4288  exmid0el  4290  exmidel  4291  exmidundif  4292  exmidundifim  4293  exmid1stab  4294  mss  4314  copsex2t  4333  euotd  4343  pwunim  4379  ispod  4397  sotricim  4416  exse  4429  frind  4445  trssord  4473  suctr  4514  pwnex  4542  eusvnf  4546  eusvnfb  4547  eusv2nf  4549  rexxfrd  4556  ralxfr2d  4557  rexxfr2d  4558  rabxfrd  4562  reuhypd  4564  eldifpw  4570  iunpw  4573  ssorduni  4581  onsucb  4597  onsucelsucr  4602  sucunielr  4604  ontriexmidim  4616  ordtri2or2exmidlem  4620  onsucelsucexmid  4624  reg2exmidlema  4628  setindel  4632  elirr  4635  orddisj  4640  en2lp  4648  suc11g  4651  ordsuc  4657  nlimsucg  4660  ordtri2or2exmid  4665  ontri2orexmidim  4666  zfregfr  4668  wessep  4672  tfi  4676  peano5  4692  limom  4708  peano2b  4709  nndceq0  4712  nnpredcl  4717  0nelrel  4768  eqrelrdv  4818  xpsspw  4834  relint  4847  relop  4876  eqbrrdva  4896  ssrelrn  4918  opeldm  4930  reldmm  4946  elres  5045  relssres  5047  elrelimasn  5098  exse2  5106  issref  5115  trin2  5124  dminss  5147  imainss  5148  rnxpid  5167  dmsn0el  5202  dmmptg  5230  relrelss  5259  cnviinm  5274  iotanul  5298  sniota  5313  dffun5r  5334  funmo  5337  funco  5362  funun  5366  fununmo  5367  fununfun  5368  funprg  5375  funtpg  5376  funtp  5378  fntpg  5381  fununi  5393  funcnvuni  5394  imadiflem  5404  imainlem  5406  funimaexglem  5408  isarep2  5412  fnunsn  5434  2elresin  5438  fnimadisj  5448  dmmptd  5458  fco  5495  funssxp  5499  fssres  5507  feu  5514  fimacnvdisj  5516  fabexg  5519  f00  5523  f0rn0  5526  f1co  5549  fores  5564  foco  5565  f1ores  5593  foimacnv  5596  f1oun  5598  fun11iun  5599  f1oco  5601  fo00  5615  brprcneu  5626  fv3  5656  relelfvdm  5665  nfvres  5669  nfunsn  5670  funfvbrb  5754  respreima  5769  dff2  5785  dff3im  5786  dffo4  5789  fvmptelcdm  5794  ffvresb  5804  f1oresrab  5806  fmptco  5807  fsn  5813  fcof  5826  fpr  5829  ftpg  5831  fsnunf  5847  fsnunfv  5848  elabrex  5891  dff1o6  5910  foeqcnvco  5924  fliftel1  5928  isores1  5948  isoini2  5953  riotasbc  5981  acexmidlemph  6004  acexmidlemcase  6006  oprabidlem  6042  brabvv  6060  eloprabga  6101  fnoprabg  6115  caovimo  6209  oprabexd  6282  uchoice  6293  fo1stresm  6317  fo2ndresm  6318  unielxp  6330  1st2ndbr  6340  opabn1stprc  6351  fmpoco  6374  1stconst  6379  2ndconst  6380  poxp  6390  spc2ed  6391  disjxp1  6394  elmpom  6396  reldmtpos  6412  tposfun  6419  dftpos4  6422  smores  6451  smores2  6453  tfrlem1  6467  tfr0dm  6481  tfrlemibxssdm  6486  tfrlemibex  6488  tfrlemiubacc  6489  tfrlemi14d  6492  tfrexlem  6493  tfri1d  6494  tfr1onlembxssdm  6502  tfr1onlembex  6504  tfr1onlemubacc  6505  tfr1onlemres  6508  tfrcllemsucfn  6512  tfrcllembxssdm  6515  tfrcllembex  6517  tfrcllemubacc  6518  tfrcllemres  6521  tfri3  6526  rdgon  6545  frecabcl  6558  frecfcllem  6563  frecrdg  6567  2oconcl  6600  nnsucelsuc  6652  nntri3or  6654  nndceq  6660  nndcel  6661  dcdifsnid  6665  ecexr  6700  brdifun  6722  ecelqsdm  6767  iinerm  6769  eroveu  6788  erovlem  6789  ecopovtrn  6794  ecopovtrng  6797  th3qlem1  6799  pmsspw  6845  map0b  6849  mapsn  6852  mapsncnv  6857  ixpf  6882  uniixp  6883  ixpexgg  6884  resixp  6895  f1oen3g  6920  ssdomg  6945  domtr  6952  snfig  6982  modom  6987  enpr2d  6990  dom1o  6995  xpf1o  7023  xpmapenlem  7028  php5dom  7042  fidceq  7049  nnfi  7052  fiunsnnn  7061  findcard  7068  findcard2  7069  findcard2s  7070  ac6sfi  7078  fidcen  7079  tridc  7080  fimax2gtri  7082  finexdc  7083  elssdc  7085  eqsndc  7086  exmidpw  7091  exmidpweq  7092  exmidpw2en  7095  nnwetri  7099  unsnfi  7102  unsnfidcex  7103  unsnfidcel  7104  undifdcss  7106  tpfidisj  7112  tpfidceq  7113  iunfidisj  7134  snexxph  7138  fidcenumlemrks  7141  sbthlem2  7146  sbthlemi3  7147  sbthlem7  7151  sbthlemi8  7152  fival  7158  dcfi  7169  supmoti  7181  djuss  7258  updjudhf  7267  updjud  7270  casefun  7273  caseinj  7277  omp1eomlem  7282  djufun  7292  djuinj  7294  ctssdccl  7299  ctfoex  7306  nnnninf  7314  nnnninfeq2  7317  nninfisollem0  7318  nninfisollemne  7319  nninfisollemeq  7320  nninfisol  7321  finomni  7328  exmidomniim  7329  exmidomni  7330  fodjuomnilemdc  7332  omniwomnimkv  7355  nninfdcinf  7359  nninfwlporlem  7361  nninfwlpoimlemg  7363  nninfwlpoim  7367  nninfinfwlpo  7368  exmidonfinlem  7392  exmidfodomrlemr  7401  exmidfodomrlemrALT  7402  finacn  7407  exmidaclem  7411  dju1en  7416  exmidontriimlem1  7424  exmidontriimlem3  7426  iftrueb01  7429  pw1on  7432  3nsssucpw1  7442  2omotaplemap  7464  2omotap  7466  exmidmotap  7468  cc4f  7476  cc4n  7478  acnccim  7479  dmaddpqlem  7585  nqpi  7586  dmaddpq  7587  dmmulpq  7588  ltdcnq  7605  subhalfnqq  7622  enq0sym  7640  enq0ref  7641  enq0tr  7642  nqnq0pi  7646  nq0nn  7650  addnq0mo  7655  mulnq0mo  7656  nqpnq0nq  7661  nqnq0a  7662  nqnq0m  7663  npsspw  7679  elnp1st2nd  7684  prnmaxl  7696  prnminu  7697  prarloc  7711  genprndl  7729  genprndu  7730  nqprm  7750  nqprl  7759  nqpru  7760  addnqprlemrl  7765  addnqprlemru  7766  prmuloc  7774  mulnqprlemrl  7781  mulnqprlemru  7782  ltsopr  7804  ltexprlemm  7808  ltexprlemopl  7809  ltexprlemopu  7811  lteupri  7825  recexprlemopl  7833  recexprlemopu  7835  recexprlemdisj  7838  archpr  7851  cauappcvgprlemdisj  7859  cauappcvgprlemladdrl  7865  cauappcvgprlem2  7868  caucvgprlemnbj  7875  caucvgprlemdisj  7882  caucvgprlemladdfu  7885  caucvgprlem2  7888  caucvgprprlemnbj  7901  caucvgprprlemdisj  7910  suplocexprlemml  7924  suplocexprlemrl  7925  suplocexprlemmu  7926  suplocexprlemloc  7929  addsrmo  7951  mulsrmo  7952  recexgt0sr  7981  prsrpos  7993  caucvgsrlemasr  7998  suplocsrlemb  8014  suplocsrlempr  8015  suplocsr  8017  elrealeu  8037  pitonn  8056  pitoregt0  8057  pitore  8058  recnnre  8059  axaddcl  8072  axaddrcl  8073  axmulcl  8074  axmulrcl  8075  axrnegex  8087  axcnre  8089  axpre-lttrn  8092  rereceu  8097  axarch  8099  axpre-suploclemres  8109  axpre-suploc  8110  ltxrlt  8233  apirr  8773  divmulasscomap  8864  rerecclap  8898  lbreu  9113  arch  9387  0mnnnnn0  9422  nnm1nn0  9431  elnnnn0c  9435  elnnz1  9490  ztri3or0  9509  nzadd  9520  nn0n0n1ge2  9538  zdceq  9543  zdcle  9544  zdclt  9545  uzind  9579  eluzge3nn  9794  supinfneg  9817  infsupneg  9818  eluz2b2  9825  elnn1uz2  9829  elnn0dc  9833  elnndc  9834  nn01to3  9839  znq  9846  qaddcl  9857  qmulcl  9859  qreccl  9864  irradd  9868  irrmul  9869  elpq  9871  cnref1o  9873  xnn0dcle  10025  xrpnfdc  10065  xrmnfdc  10066  xaddcom  10084  xnegdi  10091  xpncan  10094  xleadd1a  10096  iooidg  10132  elioo4g  10157  elfzd  10239  fzdcel  10263  fznlem  10264  fzpreddisj  10294  fz0to4untppr  10347  elfz0ubfz0  10348  elfz0fzfz0  10349  fz0fzelfz0  10350  fz0fzdiffz0  10353  elfzmlbp  10355  difelfzle  10357  4fvwrd4  10363  fzosplit  10402  elfzo0  10409  fzo1fzo0n0  10410  elfzonn0  10413  fzofzim  10415  elfzo1  10418  elfzom1elp1fzo  10435  fzossfzop1  10445  ssfzo12bi  10458  exfzdc  10474  zsupcllemstep  10477  infssuzex  10481  qdceq  10492  qdclt  10493  exbtwnzlemstep  10495  exbtwnzlemex  10497  exbtwnz  10498  rebtwn2zlemstep  10500  rebtwn2z  10502  qbtwnxr  10505  modfzo0difsn  10645  frec2uzrand  10655  frec2uzf1od  10656  frecuzrdgrcl  10660  frecuzrdgtcl  10662  frecuzrdgrclt  10665  frecuzrdgfunlem  10669  frecfzennn  10676  nninfinf  10693  seq3f1olemp  10765  seq3f1oleml  10766  seqf1oglem1  10769  ser0f  10784  expcl2lemap  10801  hashunsng  11058  iswrdinn0  11105  snopiswrd  11110  wrdlndm  11117  iswrdsymb  11118  wrdsymb1  11137  ccatfv0  11167  ccatval21sw  11169  lswccatn0lsw  11175  eqs1  11192  ccat1st1st  11205  lswccats1fst  11208  fzowrddc  11215  swrdfv0  11222  swrdlen2  11230  swrdfv2  11231  swrdsbslen  11234  swrdspsleq  11235  pfxfv0  11260  pfxtrcfv0  11262  pfxeq  11264  pfx1  11271  swrdswrdlem  11272  cats1un  11289  pfxccatin12lem2a  11295  pfxccatin12lem2  11299  pfxccatin12lem3  11300  swrdccat  11303  cats1fvn  11332  cats1fvnd  11333  shftfvalg  11366  shftfval  11369  caucvgre  11529  rexanuz  11536  recvguniq  11543  rennim  11550  resqrexlemf  11555  rsqrmo  11575  fimaxre2  11775  climeu  11844  sumdc  11906  summodc  11931  zsumdc  11932  isum  11933  fisumss  11940  isumss2  11941  fsumsplit  11955  sumsnf  11957  fsumsplitsn  11958  sumtp  11962  sumsplitdc  11980  fsum2dlemstep  11982  fisum0diag2  11995  fsumconst  12002  modfsummodlemstep  12005  fsum00  12010  fsumabs  12013  fsumiun  12025  isumlessdc  12044  expcnv  12052  prodmodc  12126  zproddc  12127  iprodap  12128  iprodap0  12130  fprodssdc  12138  prodsnf  12140  fprodsplitdc  12144  fprodsplit  12145  fprodm1  12146  fprod1p  12147  fprodunsn  12152  fprod2dlemstep  12170  fprodsplitsn  12181  ef0lem  12208  modmulconst  12371  dvdsdivcl  12398  dvdsssfz1  12400  dvdsfac  12408  zeoxor  12417  nn0ehalf  12451  nn0oddm1d2  12457  nnoddm1d2  12458  divalglemeunn  12469  divalglemeuneg  12471  bitsfzolem  12502  bitsinv1  12510  gcdsupex  12515  gcdsupcl  12516  bezoutlemnewy  12554  bezoutlemmain  12556  bezoutlemeu  12565  dfgcd2  12572  nnwosdc  12597  nninfct  12599  algrf  12604  algcvgblem  12608  lcmgcdlem  12636  lcmdvds  12638  coprmgcdb  12647  mulgcddvds  12653  qredeu  12656  cncongr1  12662  cncongr2  12663  isprm2lem  12675  dvdsnprmd  12684  prmdc  12689  oddprmge3  12694  pw2dvdseu  12727  phibndlem  12775  dfphi2  12779  hashdvds  12780  phiprmpw  12781  eulerthlemh  12790  hashgcdeq  12799  phisum  12800  odzdvds  12805  reumodprminv  12813  nnnn0modprm0  12815  prm23ge5  12824  pclemdc  12848  pcdvdsb  12880  difsqpwdvds  12898  oddprmdvds  12914  1arith  12927  4sqlem3  12950  4sqlemafi  12955  4sqlemffi  12956  4sqleminfi  12957  4sqexercise1  12958  4sqlem11  12961  4sqlem19  12969  ennnfonelemdc  13007  ennnfonelemh  13012  ennnfonelemhf1o  13021  ennnfonelemf1  13026  ennnfonelemrn  13027  ennnfonelemdm  13028  exmidunben  13034  ctinfomlemom  13035  ctinfom  13036  ctiunctlemudc  13045  ctiunctlemf  13046  ctiunctal  13049  nninfdclemcl  13056  nninfdclemf  13057  nninfdclemp1  13058  isstructim  13083  setsresg  13107  strleund  13173  1strbas  13187  2strbasg  13190  2stropg  13191  restsspw  13319  tgval  13332  ptex  13334  imasaddfnlemg  13384  fnpr2o  13409  fnpr2ob  13410  mgmidsssn0  13454  fngsum  13458  igsumvalx  13459  isnsgrp  13476  sgrpidmndm  13490  mndinvmod  13515  mnd1  13525  mhmeql  13562  grpinveu  13608  prdsinvlem  13678  mulgval  13696  subgintm  13772  trivsubgsnd  13775  eqgfval  13796  ecqusaddd  13812  ecqusaddcl  13813  ghmeql  13841  iscmnd  13872  imasabl  13910  gsumfzmhm2  13918  rnglz  13945  srgfcl  13973  rhmopp  14177  subrgdvds  14236  lssuni  14364  lssintclm  14385  lspf  14390  qusmulrng  14533  mulgrhm2  14611  znf1o  14652  psrbagfi  14674  psr1clfi  14689  mplsubgfilemcl  14700  istopon  14724  toponcom  14738  topgele  14740  topontopn  14748  tsettps  14749  eltg2b  14765  unitg  14773  tgss2  14790  bastop2  14795  distop  14796  epttop  14801  cldss2  14817  neisspw  14859  neipsm  14865  neiuni  14872  tgcn  14919  tgcnp  14920  cnntr  14936  lmff  14960  txuni2  14967  txbasex  14968  txbas  14969  txcnp  14982  txcnmpt  14984  txcn  14986  txdis  14988  txdis1cn  14989  cnmpt11  14994  cnmpt12  14998  cnmpt21  15002  cnmpt2t  15004  cnmpt22  15005  blsscls2  15204  xmetxpbl  15219  xmettxlem  15220  tgqioo  15266  fsumcncntop  15278  cncfmpt1f  15309  mulcncflem  15318  mulcncf  15319  dedekindeu  15334  dedekindicclemicc  15343  dedekindicc  15344  ivthinclemdisj  15351  hovercncf  15357  limcimo  15376  cnmptlimc  15385  reldvg  15390  dvfvalap  15392  dvfgg  15399  dvmptfsum  15436  dveflem  15437  dvef  15438  elply2  15446  sincn  15480  coscn  15481  reeff1o  15484  pilem3  15494  ioocosf1o  15565  mpodvdsmulf1o  15701  fsumdvdsmul  15702  perfectlem2  15711  lgsne0  15754  gausslemma2dlem1a  15774  gausslemma2dlem4  15780  lgseisenlem2  15787  lgseisenlem3  15788  lgsquadlem2  15794  2lgslem3  15817  2sqlem2  15831  mul2sq  15832  2sqlem3  15833  2sqlem7  15837  edgstruct  15901  pw0ss  15920  incistruhgr  15927  upgrex  15940  umgrnloop0  15954  lfgrnloopen  15968  umgredg  15980  umgrnloop2  15986  uspgredgiedg  16013  uspgriedgedg  16014  usgrislfuspgrdom  16025  usgredg3  16049  uspgredg2vlem  16055  uspgredg2v  16056  ushgredgedg  16061  ushgredgedgloop  16063  uhgr0vsize0en  16070  usgr1e  16076  vtxedgfi  16091  vtxlpfi  16092  vtxdumgrfival  16100  wlkcprim  16138  wlk1walkdom  16147  uspgr2wlkeq  16153  upgr2wlkdc  16163  wlkres  16165  clwwlkccatlem  16185  clwwlknp  16202  umgr2cwwk2dif  16209  bj-trst  16245  bj-fast  16247  bj-stand  16254  bj-trdc  16258  bj-fadc  16260  decidr  16302  djulclALT  16307  djurclALT  16308  bj-charfunr  16315  bj-indind  16437  bj-2inf  16443  bj-nntrans2  16457  bj-peano4  16460  bj-nnord  16463  bj-inf2vn  16479  bj-inf2vn2  16480  bj-findis  16484  pwf1oexmid  16510  subctctexmid  16511  pw1dceq  16515  nnsf  16517  nninfsellemdc  16522  nninffeq  16532  nnnninfen  16533  exmidsbthrlem  16536  sbthom  16540  triap  16543  trilpo  16557  apdifflemr  16561  redcwlpo  16569  tridceq  16570  nconstwlpolem0  16577  nconstwlpolem  16579  nconstwlpo  16580  neapmkv  16582  ltlenmkv  16584