Theorem sylibr 132

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 131	. 2 ⊢ (𝜓 → 𝜒)
4	1, 3	syl 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sylbbr  134  pm5.74rd  181  bitri  182  3imtr4i  199  sylanbrc  408  dcimpstab  785  dcim  817  oibabs  833  stabtestimpdc  857  dcor  876  3mix1  1107  3mix2  1108  3jca  1118  syl3anbrc  1122  inegd  1303  pclem6  1305  xoranor  1308  nfxfrd  1404  nfd  1456  hban  1479  nfan1  1496  nford  1499  nfand  1500  hbim1  1502  alexim  1576  ax6blem  1580  nf4r  1601  19.34  1614  nfexd  1684  sbcof2  1731  nfsb2or  1758  sbidm  1772  nfdv  1798  nfeudv  1956  mon  1970  eumo  1973  mo23  1982  eu2  1985  eu3h  1986  exmodc  1991  exmonim  1992  mo2r  1993  mo3h  1994  bm1.1  2066  eqrdv  2079  3eltr4g  2164  abbi2dv  2197  abbi1dv  2198  nfcd  2214  nfcxfrd  2217  dcned  2251  neqned  2252  3netr4g  2280  necon3bi  2295  necon2ai  2299  alral  2409  rspe  2412  rsp2e  2414  rgen2a  2417  ralrimi  2432  r19.27av  2492  r19.32r  2501  nfreudxy  2527  mormo  2565  nrexrmo  2570  cgsex2g  2635  cgsex4g  2636  spc2egv  2687  spc2gv  2688  spc3egv  2689  spc3gv  2690  rspce  2696  ceqex  2722  elrab3t  2748  mosubt  2769  mo2icl  2771  reu3  2782  reu6i  2783  2rmorex  2796  sbc5  2838  rspesbca  2898  rmo2ilem  2903  sbnfc2  2962  ssrd  3004  ssrdv  3005  3sstr4g  3040  syl5eqss  3043  ss2abdv  3067  abssdv  3068  rabssdv  3074  ss2rabdv  3075  ssun1  3135  unssad  3149  unssbd  3150  ssddif  3198  uneqin  3215  indifdir  3220  undif3ss  3225  reuss2  3244  n0rf  3260  reximdva0m  3263  rabxmdc  3276  ssindif0im  3303  minel  3305  ralidm  3341  ralm  3345  disjsn2  3455  absneu  3464  rabsneu  3465  opprc  3591  elunii  3606  dfnfc2  3619  uniss2  3632  unidif  3633  ssunieq  3634  intab  3665  iunss2  3723  iunxdif2  3726  invdisj  3780  3brtr4g  3817  trin  3885  triun  3888  truni  3889  trint  3890  iinexgm  3929  class2seteq  3937  pwuni  3963  mss  3981  copsex2t  4000  euotd  4009  pwunim  4041  ispod  4059  sotricim  4078  exse  4091  frind  4107  trssord  4135  suctr  4176  eusvnf  4203  eusvnfb  4204  eusv2nf  4206  rexxfrd  4213  ralxfr2d  4214  rexxfr2d  4215  rabxfrd  4219  reuhypd  4221  eldifpw  4226  iunpw  4229  ssorduni  4231  sucelon  4247  onsucelsucr  4252  sucunielr  4254  ordtri2or2exmidlem  4269  onsucelsucexmid  4273  reg2exmidlema  4277  setindel  4281  elirr  4284  orddisj  4289  en2lp  4297  suc11g  4300  ordsuc  4306  nlimsucg  4309  ordtri2or2exmid  4314  zfregfr  4316  wessep  4320  tfi  4323  peano5  4339  limom  4354  peano2b  4355  nndceq0  4357  eqrelrdv  4454  xpsspw  4468  relint  4479  relop  4504  eqbrrdva  4523  opeldm  4556  elres  4664  relssres  4666  exse2  4719  issref  4727  trin2  4736  dminss  4758  imainss  4759  rnxpid  4775  dmsn0el  4810  dmmptg  4838  relrelss  4864  cnviinm  4879  iotanul  4902  sniota  4914  dffun5r  4934  funmo  4937  funco  4960  funun  4964  funprg  4969  funtpg  4970  funtp  4972  fntpg  4975  fununi  4987  funcnvuni  4988  imadiflem  4998  imainlem  5000  funimaexglem  5002  isarep2  5006  fnunsn  5026  2elresin  5030  fnimadisj  5039  fco  5076  funssxp  5080  fssres  5086  feu  5092  fimacnvdisj  5094  fabexg  5097  f00  5101  f1co  5121  fores  5135  foco  5136  f1ores  5161  foimacnv  5164  f1oun  5166  fun11iun  5167  f1oco  5169  fo00  5182  brprcneu  5191  fv3  5218  relelfvdm  5226  nfvres  5227  nfunsn  5228  funfvbrb  5301  respreima  5316  dff2  5332  dff3im  5333  dffo4  5336  ffvresb  5349  f1oresrab  5350  fmptco  5351  fsn  5356  fpr  5366  ftpg  5368  fsnunf  5383  fsnunfv  5384  elabrex  5418  dff1o6  5436  foeqcnvco  5450  fliftel1  5454  isores1  5474  isoini2  5478  riotasbc  5503  acexmidlemph  5525  acexmidlemcase  5527  oprabidlem  5556  brabvv  5571  eloprabga  5611  fnoprabg  5622  caovimo  5714  oprabexd  5774  fo1stresm  5808  fo2ndresm  5809  unielxp  5820  1st2ndbr  5830  fmpt2co  5857  1stconst  5862  2ndconst  5863  poxp  5873  spc2ed  5874  reldmtpos  5891  tposfun  5898  dftpos4  5901  smores  5930  smores2  5932  tfrlem1  5946  tfr0  5960  tfrlemibxssdm  5964  tfrlemibex  5966  tfrlemiubacc  5967  tfrlemi14d  5970  tfrexlem  5971  tfri1d  5972  tfri3  5976  2oconcl  6045  nnsucelsuc  6093  nntri3or  6095  nndceq  6100  nndcel  6101  nndifsnid  6103  ecexr  6134  brdifun  6156  ecelqsdm  6199  iinerm  6201  eroveu  6220  erovlem  6221  ecopovtrn  6226  ecopovtrng  6229  th3qlem1  6231  f1oen3g  6257  ssdomg  6281  domtr  6288  snfig  6314  php5dom  6349  fidceq  6354  fidifsnid  6356  nnfi  6357  fiunsnnn  6365  findcard  6372  findcard2  6373  findcard2s  6374  ac6sfi  6379  nnwetri  6382  unsnfi  6384  unsnfidcex  6385  unsnfidcel  6386  supmoti  6406  dmaddpqlem  6567  nqpi  6568  dmaddpq  6569  dmmulpq  6570  ltdcnq  6587  subhalfnqq  6604  enq0sym  6622  enq0ref  6623  enq0tr  6624  nqnq0pi  6628  nq0nn  6632  addnq0mo  6637  mulnq0mo  6638  nqpnq0nq  6643  nqnq0a  6644  nqnq0m  6645  npsspw  6661  elnp1st2nd  6666  prnmaxl  6678  prnminu  6679  prarloc  6693  genprndl  6711  genprndu  6712  nqprm  6732  nqprl  6741  nqpru  6742  addnqprlemrl  6747  addnqprlemru  6748  prmuloc  6756  mulnqprlemrl  6763  mulnqprlemru  6764  ltsopr  6786  ltexprlemm  6790  ltexprlemopl  6791  ltexprlemopu  6793  lteupri  6807  recexprlemopl  6815  recexprlemopu  6817  recexprlemdisj  6820  archpr  6833  cauappcvgprlemdisj  6841  cauappcvgprlemladdrl  6847  cauappcvgprlem2  6850  caucvgprlemnbj  6857  caucvgprlemdisj  6864  caucvgprlemladdfu  6867  caucvgprlem2  6870  caucvgprprlemnbj  6883  caucvgprprlemdisj  6892  addsrmo  6920  mulsrmo  6921  recexgt0sr  6950  prsrpos  6961  caucvgsrlemasr  6966  elrealeu  6998  pitonn  7016  pitoregt0  7017  pitore  7018  recnnre  7019  axaddcl  7032  axaddrcl  7033  axmulcl  7034  axmulrcl  7035  axrnegex  7045  axcnre  7047  axpre-lttrn  7050  rereceu  7055  axarch  7057  ltxrlt  7178  apirr  7705  divmulasscomap  7784  rerecclap  7818  lbreu  8023  arch  8285  0mnnnnn0  8320  nnm1nn0  8329  elnnnn0c  8333  elnnz1  8374  ztri3or0  8393  nzadd  8403  nn0n0n1ge2  8418  zdceq  8423  zdcle  8424  zdclt  8425  uzind  8458  eluzge3nn  8660  supinfneg  8683  infsupneg  8684  eluz2b2  8690  elnn1uz2  8694  nn01to3  8702  znq  8709  qaddcl  8720  qmulcl  8722  qreccl  8727  irradd  8731  irrmul  8732  cnref1o  8733  iooidg  8932  elioo4g  8957  fzdcel  9059  fznlem  9060  fzpreddisj  9088  elfz0ubfz0  9136  elfz0fzfz0  9137  fz0fzelfz0  9138  fz0fzdiffz0  9141  elfzmlbp  9143  difelfzle  9145  4fvwrd4  9150  fzosplit  9186  elfzo0  9191  fzo1fzo0n0  9192  elfzonn0  9195  fzofzim  9197  elfzo1  9199  elfzom1elp1fzo  9211  fzossfzop1  9221  ssfzo12bi  9234  exfzdc  9249  qdceq  9256  qbtwnzlemstep  9257  qbtwnzlemex  9259  qbtwnz  9260  rebtwn2zlemstep  9261  rebtwn2z  9263  qbtwnxr  9266  modfzo0difsn  9397  frec2uzrand  9407  frec2uzf1od  9408  frecuzrdgrom  9412  frecuzrdgfn  9414  frecfzennn  9419  iseqf  9444  iser0f  9472  expcl2lemap  9488  shftfvalg  9706  shftfval  9709  caucvgre  9867  rexanuz  9874  recvguniq  9881  rennim  9888  resqrexlemf  9893  rsqrmo  9913  fimaxre2  10109  climeu  10135  modmulconst  10227  dvdsdivcl  10250  dvdsssfz1  10252  dvdsfac  10260  zeoxor  10268  nn0ehalf  10303  nn0oddm1d2  10309  nnoddm1d2  10310  divalglemeunn  10321  divalglemeuneg  10323  zsupcllemstep  10341  infssuzex  10345  gcdsupex  10349  gcdsupcl  10350  bezoutlemnewy  10385  bezoutlemmain  10387  bezoutlemeu  10396  dfgcd2  10403  ialgrf  10427  algcvgblem  10431  lcmgcdlem  10459  lcmdvds  10461  coprmgcdb  10470  mulgcddvds  10476  qredeu  10479  cncongr1  10485  cncongr2  10486  isprm2lem  10498  dvdsnprmd  10507  oddprmge3  10516  pw2dvdseu  10546  bj-nfalt  10575  bj-indind  10727  bj-2inf  10733  bj-nntrans2  10747  bj-peano4  10750  bj-nnord  10753  bj-inf2vn  10769  bj-inf2vn2  10770  bj-findis  10774