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  700  oibabs  722  dcim  849  dcstab  852  stdcndc  853  stdcndcOLD  854  dcand  941  dcor  944  dfifp2dc  990  3mix1  1193  3mix2  1194  3jca  1204  syl3anbrc  1208  syl21anbrc  1209  inegd  1417  pclem6  1419  xoranor  1422  dcfrompeirce  1495  nfxfrd  1524  nfd  1572  hban  1596  nfan1  1613  nford  1616  nfand  1617  hbim1  1619  nfal  1625  alexim  1694  nnal  1698  hbn  1699  nf4r  1719  19.34  1732  nfexd  1809  sbcof2  1858  nfsb2or  1885  sbidm  1899  nfdv  1925  nfd2  2075  nfeudv  2094  mon  2108  eumo  2111  mo23  2121  eu2  2124  eu3h  2125  exmodc  2130  exmonim  2131  mo2r  2132  mo3h  2133  bm1.1  2216  eqrdv  2229  3eltr4g  2317  abbi2dv  2351  abbi1dv  2352  nfcd  2370  nfcxfrd  2373  dcned  2409  neqned  2410  3netr4g  2438  necon3bi  2453  necon2ai  2457  nnral  2523  alral  2578  rspe  2582  rsp2e  2584  rgen2a  2587  ralrimi  2604  r19.27v  2661  r19.28v  2662  r19.27av  2669  r19.32r  2680  nfreudxy  2708  mormo  2751  nrexrmo  2756  cgsex2g  2840  cgsex4g  2841  spc2egv  2897  spc2gv  2898  spc3egv  2899  spc3gv  2900  rspce  2906  ceqex  2934  elrab3t  2962  elrabd  2965  mosubt  2984  mo2icl  2986  reu3  2997  reu6i  2998  2rmorex  3013  sbc5  3056  rspesbca  3118  rmo2ilem  3123  sbnfc2  3189  ssrd  3233  ssrdv  3234  3sstr4g  3271  eqsstrid  3274  ss2abdv  3301  abssdv  3302  rabssdv  3308  ss2rabdv  3309  ssun1  3372  unssad  3386  unssbd  3387  ssddif  3443  uneqin  3460  indifdir  3465  undif3ss  3470  reuss2  3489  n0rf  3509  reximdva0m  3512  rabxmdc  3528  ssindif0im  3556  minel  3558  ralidm  3597  ralm  3600  dcun  3606  ifmdc  3652  disjsn2  3736  rabsnif  3742  absneu  3747  rabsneu  3748  opprc  3888  elunii  3903  dfnfc2  3916  uniss2  3929  unidif  3930  ssunieq  3931  intab  3962  iunss2  4020  iunssd  4021  iunxdif2  4024  invdisj  4086  disjiun  4088  3brtr4g  4127  trin  4202  triun  4205  truni  4206  trint  4207  iinexgm  4249  class2seteq  4259  pwuni  4288  exmid1dc  4296  exmidn0m  4297  exmidsssn  4298  exmid0el  4300  exmidel  4301  exmidundif  4302  exmidundifim  4303  exmid1stab  4304  mss  4324  copsex2t  4343  euotd  4353  pwunim  4389  ispod  4407  sotricim  4426  exse  4439  frind  4455  trssord  4483  suctr  4524  pwnex  4552  eusvnf  4556  eusvnfb  4557  eusv2nf  4559  rexxfrd  4566  ralxfr2d  4567  rexxfr2d  4568  rabxfrd  4572  reuhypd  4574  eldifpw  4580  iunpw  4583  ssorduni  4591  onsucb  4607  onsucelsucr  4612  sucunielr  4614  ontriexmidim  4626  ordtri2or2exmidlem  4630  onsucelsucexmid  4634  reg2exmidlema  4638  setindel  4642  elirr  4645  orddisj  4650  en2lp  4658  suc11g  4661  ordsuc  4667  nlimsucg  4670  ordtri2or2exmid  4675  ontri2orexmidim  4676  zfregfr  4678  wessep  4682  tfi  4686  peano5  4702  limom  4718  peano2b  4719  nndceq0  4722  nnpredcl  4727  0nelrel  4778  eqrelrdv  4828  xpsspw  4844  relint  4857  relop  4886  eqbrrdva  4906  ssrelrn  4928  opeldm  4940  reldmm  4956  elres  5055  relssres  5057  elrelimasn  5109  exse2  5117  issref  5126  trin2  5135  dminss  5158  imainss  5159  rnxpid  5178  dmsn0el  5213  dmmptg  5241  relrelss  5270  cnviinm  5285  iotanul  5309  sniota  5324  dffun5r  5345  funmo  5348  funco  5373  funun  5378  fununmo  5379  fununfun  5380  funprg  5387  funtpg  5388  funtp  5390  fntpg  5393  fununi  5405  funcnvuni  5406  imadiflem  5416  imainlem  5418  funimaexglem  5420  isarep2  5424  fnunsn  5446  2elresin  5450  fnimadisj  5460  dmmptd  5470  fco  5507  funssxp  5512  fssres  5520  feu  5527  fimacnvdisj  5529  fabexg  5532  f00  5537  f0rn0  5540  f1co  5563  fores  5578  foco  5579  f1ores  5607  foimacnv  5610  f1oun  5612  fun11iun  5613  f1oco  5615  fo00  5630  brprcneu  5641  fv3  5671  relelfvdm  5680  nfvres  5684  nfunsn  5685  funfvbrb  5769  respreima  5783  dff2  5799  dff3im  5800  dffo4  5803  fvmptelcdm  5808  ffvresb  5818  f1oresrab  5820  fmptco  5821  fsn  5827  fcof  5841  fpr  5844  ftpg  5846  fsnunf  5862  fsnunfv  5863  elabrex  5908  dff1o6  5927  foeqcnvco  5941  fliftel1  5945  isores1  5965  isoini2  5970  riotasbc  5998  acexmidlemph  6021  acexmidlemcase  6023  oprabidlem  6059  brabvv  6077  eloprabga  6118  fnoprabg  6132  caovimo  6226  oprabexd  6298  uchoice  6309  fo1stresm  6333  fo2ndresm  6334  unielxp  6346  1st2ndbr  6356  opabn1stprc  6367  fmpoco  6390  1stconst  6395  2ndconst  6396  poxp  6406  spc2ed  6407  disjxp1  6410  elmpom  6412  suppsnopdc  6428  reldmtpos  6462  tposfun  6469  dftpos4  6472  smores  6501  smores2  6503  tfrlem1  6517  tfr0dm  6531  tfrlemibxssdm  6536  tfrlemibex  6538  tfrlemiubacc  6539  tfrlemi14d  6542  tfrexlem  6543  tfri1d  6544  tfr1onlembxssdm  6552  tfr1onlembex  6554  tfr1onlemubacc  6555  tfr1onlemres  6558  tfrcllemsucfn  6562  tfrcllembxssdm  6565  tfrcllembex  6567  tfrcllemubacc  6568  tfrcllemres  6571  tfri3  6576  rdgon  6595  frecabcl  6608  frecfcllem  6613  frecrdg  6617  2oconcl  6650  nnsucelsuc  6702  nntri3or  6704  nndceq  6710  nndcel  6711  dcdifsnid  6715  ecexr  6750  brdifun  6772  ecelqsdm  6817  iinerm  6819  eroveu  6838  erovlem  6839  ecopovtrn  6844  ecopovtrng  6847  th3qlem1  6849  pmsspw  6895  map0b  6899  mapsn  6902  mapsncnv  6907  ixpf  6932  uniixp  6933  ixpexgg  6934  resixp  6945  f1oen3g  6970  ssdomg  6995  domtr  7002  snfig  7032  modom  7037  enpr2d  7040  dom1o  7045  xpf1o  7073  xpmapenlem  7078  php5dom  7092  fidceq  7099  nnfi  7102  fiunsnnn  7113  findcard  7120  findcard2  7121  findcard2s  7122  ac6sfi  7130  fidcen  7131  tridc  7132  fimax2gtri  7134  finexdc  7135  elssdc  7137  eqsndc  7138  exmidpw  7143  exmidpweq  7144  exmidpw2en  7147  nnwetri  7151  unsnfi  7154  unsnfidcex  7155  unsnfidcel  7156  undifdcss  7158  tpfidisj  7164  tpfidceq  7165  exmidssfi  7174  iunfidisj  7188  snexxph  7192  fidcenumlemrks  7195  sbthlem2  7200  sbthlemi3  7201  sbthlem7  7205  sbthlemi8  7206  fival  7212  dcfi  7223  supmoti  7235  djuss  7312  updjudhf  7321  updjud  7324  casefun  7327  caseinj  7331  omp1eomlem  7336  djufun  7346  djuinj  7348  ctssdccl  7353  ctfoex  7360  nnnninf  7368  nnnninfeq2  7371  nninfisollem0  7372  nninfisollemne  7373  nninfisollemeq  7374  nninfisol  7375  finomni  7382  exmidomniim  7383  exmidomni  7384  fodjuomnilemdc  7386  omniwomnimkv  7409  nninfdcinf  7413  nninfwlporlem  7415  nninfwlpoimlemg  7417  nninfwlpoim  7421  nninfinfwlpo  7422  exmidonfinlem  7447  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  finacn  7462  exmidaclem  7466  dju1en  7471  exmidontriimlem1  7479  exmidontriimlem3  7481  iftrueb01  7484  pw1on  7487  3nsssucpw1  7497  2omotaplemap  7519  2omotap  7521  exmidmotap  7523  cc4f  7531  cc4n  7533  acnccim  7534  dmaddpqlem  7640  nqpi  7641  dmaddpq  7642  dmmulpq  7643  ltdcnq  7660  subhalfnqq  7677  enq0sym  7695  enq0ref  7696  enq0tr  7697  nqnq0pi  7701  nq0nn  7705  addnq0mo  7710  mulnq0mo  7711  nqpnq0nq  7716  nqnq0a  7717  nqnq0m  7718  npsspw  7734  elnp1st2nd  7739  prnmaxl  7751  prnminu  7752  prarloc  7766  genprndl  7784  genprndu  7785  nqprm  7805  nqprl  7814  nqpru  7815  addnqprlemrl  7820  addnqprlemru  7821  prmuloc  7829  mulnqprlemrl  7836  mulnqprlemru  7837  ltsopr  7859  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemopu  7866  lteupri  7880  recexprlemopl  7888  recexprlemopu  7890  recexprlemdisj  7893  archpr  7906  cauappcvgprlemdisj  7914  cauappcvgprlemladdrl  7920  cauappcvgprlem2  7923  caucvgprlemnbj  7930  caucvgprlemdisj  7937  caucvgprlemladdfu  7940  caucvgprlem2  7943  caucvgprprlemnbj  7956  caucvgprprlemdisj  7965  suplocexprlemml  7979  suplocexprlemrl  7980  suplocexprlemmu  7981  suplocexprlemloc  7984  addsrmo  8006  mulsrmo  8007  recexgt0sr  8036  prsrpos  8048  caucvgsrlemasr  8053  suplocsrlemb  8069  suplocsrlempr  8070  suplocsr  8072  elrealeu  8092  pitonn  8111  pitoregt0  8112  pitore  8113  recnnre  8114  axaddcl  8127  axaddrcl  8128  axmulcl  8129  axmulrcl  8130  axrnegex  8142  axcnre  8144  axpre-lttrn  8147  rereceu  8152  axarch  8154  axpre-suploclemres  8164  axpre-suploc  8165  ltxrlt  8288  apirr  8828  divmulasscomap  8919  rerecclap  8953  lbreu  9168  arch  9442  0mnnnnn0  9477  nnm1nn0  9486  elnnnn0c  9490  elnnz1  9545  ztri3or0  9564  nzadd  9575  nn0n0n1ge2  9593  zdceq  9598  zdcle  9599  zdclt  9600  uzind  9634  eluzge3nn  9849  supinfneg  9872  infsupneg  9873  eluz2b2  9880  elnn1uz2  9884  elnn0dc  9888  elnndc  9889  nn01to3  9894  znq  9901  qaddcl  9912  qmulcl  9914  qreccl  9919  irradd  9923  irrmul  9924  elpq  9926  cnref1o  9928  xnn0dcle  10080  xrpnfdc  10120  xrmnfdc  10121  xaddcom  10139  xnegdi  10146  xpncan  10149  xleadd1a  10151  iooidg  10187  elioo4g  10212  elfzd  10294  fzdcel  10318  fznlem  10319  fzpreddisj  10349  fz0to4untppr  10402  elfz0ubfz0  10403  elfz0fzfz0  10404  fz0fzelfz0  10405  fz0fzdiffz0  10408  elfzmlbp  10410  difelfzle  10412  4fvwrd4  10418  fzosplit  10457  elfzo0  10464  nn0p1elfzo  10465  fzo1fzo0n0  10466  elfzonn0  10469  fzofzim  10471  elfzo1  10474  elfzom1elp1fzo  10491  fzossfzop1  10501  ssfzo12bi  10514  exfzdc  10530  zsupcllemstep  10533  infssuzex  10537  qdceq  10548  qdclt  10549  exbtwnzlemstep  10551  exbtwnzlemex  10553  exbtwnz  10554  rebtwn2zlemstep  10556  rebtwn2z  10558  qbtwnxr  10561  modfzo0difsn  10701  frec2uzrand  10711  frec2uzf1od  10712  frecuzrdgrcl  10716  frecuzrdgtcl  10718  frecuzrdgrclt  10721  frecuzrdgfunlem  10725  frecfzennn  10732  nninfinf  10749  seq3f1olemp  10821  seq3f1oleml  10822  seqf1oglem1  10825  ser0f  10840  expcl2lemap  10857  hashunsng  11115  iswrdinn0  11165  snopiswrd  11170  wrdlndm  11177  iswrdsymb  11178  wrdsymb1  11197  ccatfv0  11227  ccatval21sw  11229  lswccatn0lsw  11235  eqs1  11252  ccat1st1st  11265  lswccats1fst  11268  fzowrddc  11275  swrdfv0  11282  swrdlen2  11290  swrdfv2  11291  swrdsbslen  11294  swrdspsleq  11295  pfxfv0  11320  pfxtrcfv0  11322  pfxeq  11324  pfx1  11331  swrdswrdlem  11332  cats1un  11349  pfxccatin12lem2a  11355  pfxccatin12lem2  11359  pfxccatin12lem3  11360  swrdccat  11363  cats1fvn  11392  cats1fvnd  11393  shftfvalg  11439  shftfval  11442  caucvgre  11602  rexanuz  11609  recvguniq  11616  rennim  11623  resqrexlemf  11628  rsqrmo  11648  fimaxre2  11848  climeu  11917  sumdc  11979  summodc  12005  zsumdc  12006  isum  12007  fisumss  12014  isumss2  12015  fsumsplit  12029  sumsnf  12031  fsumsplitsn  12032  sumtp  12036  sumsplitdc  12054  fsum2dlemstep  12056  fisum0diag2  12069  fsumconst  12076  modfsummodlemstep  12079  fsum00  12084  fsumabs  12087  fsumiun  12099  isumlessdc  12118  expcnv  12126  prodmodc  12200  zproddc  12201  iprodap  12202  iprodap0  12204  fprodssdc  12212  prodsnf  12214  fprodsplitdc  12218  fprodsplit  12219  fprodm1  12220  fprod1p  12221  fprodunsn  12226  fprod2dlemstep  12244  fprodsplitsn  12255  ef0lem  12282  modmulconst  12445  dvdsdivcl  12472  dvdsssfz1  12474  dvdsfac  12482  zeoxor  12491  nn0ehalf  12525  nn0oddm1d2  12531  nnoddm1d2  12532  divalglemeunn  12543  divalglemeuneg  12545  bitsfzolem  12576  bitsinv1  12584  gcdsupex  12589  gcdsupcl  12590  bezoutlemnewy  12628  bezoutlemmain  12630  bezoutlemeu  12639  dfgcd2  12646  nnwosdc  12671  nninfct  12673  algrf  12678  algcvgblem  12682  lcmgcdlem  12710  lcmdvds  12712  coprmgcdb  12721  mulgcddvds  12727  qredeu  12730  cncongr1  12736  cncongr2  12737  isprm2lem  12749  dvdsnprmd  12758  prmdc  12763  oddprmge3  12768  pw2dvdseu  12801  phibndlem  12849  dfphi2  12853  hashdvds  12854  phiprmpw  12855  eulerthlemh  12864  hashgcdeq  12873  phisum  12874  odzdvds  12879  reumodprminv  12887  nnnn0modprm0  12889  prm23ge5  12898  pclemdc  12922  pcdvdsb  12954  difsqpwdvds  12972  oddprmdvds  12988  1arith  13001  4sqlem3  13024  4sqlemafi  13029  4sqlemffi  13030  4sqleminfi  13031  4sqexercise1  13032  4sqlem11  13035  4sqlem19  13043  ennnfonelemdc  13081  ennnfonelemh  13086  ennnfonelemhf1o  13095  ennnfonelemf1  13100  ennnfonelemrn  13101  ennnfonelemdm  13102  exmidunben  13108  ctinfomlemom  13109  ctinfom  13110  ctiunctlemudc  13119  ctiunctlemf  13120  ctiunctal  13123  nninfdclemcl  13130  nninfdclemf  13131  nninfdclemp1  13132  isstructim  13157  setsresg  13181  strleund  13247  1strbas  13261  2strbasg  13264  2stropg  13265  restsspw  13393  tgval  13406  ptex  13408  imasaddfnlemg  13458  fnpr2o  13483  fnpr2ob  13484  mgmidsssn0  13528  fngsum  13532  igsumvalx  13533  isnsgrp  13550  sgrpidmndm  13564  mndinvmod  13589  mnd1  13599  mhmeql  13636  grpinveu  13682  prdsinvlem  13752  mulgval  13770  subgintm  13846  trivsubgsnd  13849  eqgfval  13870  ecqusaddd  13886  ecqusaddcl  13887  ghmeql  13915  iscmnd  13946  imasabl  13984  gsumfzmhm2  13992  rnglz  14020  srgfcl  14048  rhmopp  14252  subrgdvds  14311  lssuni  14439  lssintclm  14460  lspf  14465  qusmulrng  14608  mulgrhm2  14686  znf1o  14727  psrbagfi  14750  psrbagconcl  14753  psr1clfi  14769  mplsubgfilemcl  14780  istopon  14804  toponcom  14818  topgele  14820  topontopn  14828  tsettps  14829  eltg2b  14845  unitg  14853  tgss2  14870  bastop2  14875  distop  14876  epttop  14881  cldss2  14897  neisspw  14939  neipsm  14945  neiuni  14952  tgcn  14999  tgcnp  15000  cnntr  15016  lmff  15040  txuni2  15047  txbasex  15048  txbas  15049  txcnp  15062  txcnmpt  15064  txcn  15066  txdis  15068  txdis1cn  15069  cnmpt11  15074  cnmpt12  15078  cnmpt21  15082  cnmpt2t  15084  cnmpt22  15085  blsscls2  15284  xmetxpbl  15299  xmettxlem  15300  tgqioo  15346  fsumcncntop  15358  cncfmpt1f  15389  mulcncflem  15398  mulcncf  15399  dedekindeu  15414  dedekindicclemicc  15423  dedekindicc  15424  ivthinclemdisj  15431  hovercncf  15437  limcimo  15456  cnmptlimc  15465  reldvg  15470  dvfvalap  15472  dvfgg  15479  dvmptfsum  15516  dveflem  15517  dvef  15518  elply2  15526  sincn  15560  coscn  15561  reeff1o  15564  pilem3  15574  ioocosf1o  15645  mpodvdsmulf1o  15784  fsumdvdsmul  15785  perfectlem2  15794  lgsne0  15837  gausslemma2dlem1a  15857  gausslemma2dlem4  15863  lgseisenlem2  15870  lgseisenlem3  15871  lgsquadlem2  15877  2lgslem3  15900  2sqlem2  15914  mul2sq  15915  2sqlem3  15916  2sqlem7  15920  edgstruct  15985  pw0ss  16004  incistruhgr  16011  upgrex  16024  umgrnloop0  16038  upgr1een  16045  lfgrnloopen  16054  umgredg  16066  umgrnloop2  16072  uspgredgiedg  16099  uspgriedgedg  16100  usgrislfuspgrdom  16111  usgredg3  16135  uspgredg2vlem  16141  uspgredg2v  16142  ushgredgedg  16147  ushgredgedgloop  16149  uhgr0vsize0en  16156  usgr1e  16162  subusgr  16196  vtxedgfi  16210  vtxlpfi  16211  vtxdumgrfival  16219  1loopgrvd2fi  16226  p1evtxdeqfilem  16232  vdegp1aid  16235  wlkcprim  16271  wlk1walkdom  16280  uspgr2wlkeq  16286  upgr2wlkdc  16298  wlkres  16300  clwwlkccatlem  16321  clwwlknp  16338  umgr2cwwk2dif  16345  trlsegvdegfi  16388  eupth2lem3lem3fi  16391  eupth2lem3lem6fi  16392  eupth2lem3lem4fi  16394  eupth2lembfi  16398  depindlem1  16427  bj-trst  16437  bj-fast  16439  bj-stand  16446  bj-trdc  16450  bj-fadc  16452  decidr  16494  djulclALT  16499  djurclALT  16500  bj-charfunr  16506  bj-indind  16628  bj-2inf  16634  bj-nntrans2  16648  bj-peano4  16651  bj-nnord  16654  bj-inf2vn  16670  bj-inf2vn2  16671  bj-findis  16675  pwf1oexmid  16701  subctctexmid  16702  pw1dceq  16706  exmidnotnotr  16707  exmidcon  16708  exmidpeirce  16709  nnsf  16711  nninfsellemdc  16716  nninffeq  16726  nnnninfen  16727  exmidsbthrlem  16730  sbthom  16734  triap  16741  trilpo  16755  apdifflemr  16759  redcwlpo  16768  tridceq  16769  nconstwlpolem0  16776  nconstwlpolem  16778  nconstwlpo  16779  neapmkv  16781  ltlenmkv  16783  gfsump1  16795