Theorem sylibr 137

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

Syntax hints:   → wi 4   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm5.74rd  172  bitri  173  3imtr4i  190  sylanbrc  394  dcimpstab  752  dcim  784  oibabs  800  stabtestimpdc  824  dcor  843  3mix1  1073  3mix2  1074  3jca  1084  syl3anbrc  1088  inegd  1263  pclem6  1265  xoranor  1268  nfxfrd  1364  nfd  1416  hban  1439  nfan1  1456  nford  1459  nfand  1460  hbim1  1462  alexim  1536  ax6blem  1540  nf4r  1561  19.34  1574  nfexd  1644  sbcof2  1691  nfsb2or  1718  sbidm  1731  nfdv  1757  nfeudv  1915  mon  1929  eumo  1932  mo23  1941  eu2  1944  eu3h  1945  exmodc  1950  exmonim  1951  mo2r  1952  mo3h  1953  bm1.1  2025  eqrdv  2038  3eltr4g  2123  abbi2dv  2156  abbi1dv  2157  nfcd  2173  nfcxfrd  2176  dcned  2212  neqned  2213  3netr4g  2240  necon3bi  2255  necon2ai  2259  alral  2367  rspe  2370  rsp2e  2372  rgen2a  2375  ralrimi  2390  r19.27av  2448  r19.32r  2457  nfreudxy  2483  mormo  2521  nrexrmo  2526  cgsex2g  2590  cgsex4g  2591  spc2egv  2642  spc2gv  2643  spc3egv  2644  spc3gv  2645  rspce  2651  ceqex  2671  elrab3t  2697  mosubt  2718  mo2icl  2720  reu3  2731  reu6i  2732  2rmorex  2745  sbc5  2787  rspesbca  2842  rmo2ilem  2847  sbnfc2  2906  ssrd  2950  ssrdv  2951  3sstr4g  2986  syl5eqss  2989  ss2abdv  3013  abssdv  3014  rabssdv  3020  ss2rabdv  3021  ssun1  3106  unssad  3120  unssbd  3121  ssddif  3171  uneqin  3188  indifdir  3193  undif3ss  3198  reuss2  3217  n0rf  3233  reximdva0m  3236  rabxmdc  3249  ssindif0im  3281  minel  3283  ralidm  3321  ralm  3325  disjsn2  3433  absneu  3442  rabsneu  3443  opprc  3570  elunii  3585  dfnfc2  3598  uniss2  3611  unidif  3612  ssunieq  3613  intab  3644  iunss2  3702  iunxdif2  3705  invdisj  3759  3brtr4g  3796  trin  3864  triun  3867  truni  3868  trint  3869  iinexgm  3908  class2seteq  3916  pwuni  3943  mss  3962  copsex2t  3982  euotd  3991  pwunim  4023  ispod  4041  sotricim  4060  exse  4073  frind  4089  trssord  4117  suctr  4158  eusvnf  4185  eusvnfb  4186  eusv2nf  4188  rexxfrd  4195  ralxfr2d  4196  rexxfr2d  4197  rabxfrd  4201  reuhypd  4203  eldifpw  4208  iunpw  4211  ssorduni  4213  sucelon  4229  onsucelsucr  4234  sucunielr  4236  ordtri2or2exmidlem  4251  onsucelsucexmid  4255  reg2exmidlema  4259  setindel  4263  elirr  4266  orddisj  4270  en2lp  4278  suc11g  4281  ordsuc  4287  nlimsucg  4290  onpsssuc  4295  ordtri2or2exmid  4296  zfregfr  4298  wessep  4302  tfi  4305  peano5  4321  limom  4336  peano2b  4337  nndceq0  4339  eqrelrdv  4436  xpsspw  4450  relint  4461  relop  4486  eqbrrdva  4505  opeldm  4538  elres  4646  relssres  4648  exse2  4699  issref  4707  trin2  4716  dminss  4738  imainss  4739  rnxpid  4755  dmsn0el  4790  dmmptg  4818  relrelss  4844  cnviinm  4859  iotanul  4882  sniota  4894  dffun5r  4914  funmo  4917  funco  4940  funun  4944  funprg  4949  funtpg  4950  funtp  4952  fntpg  4955  fununi  4967  funcnvuni  4968  imadiflem  4978  imainlem  4980  funimaexglem  4982  isarep2  4986  fnunsn  5006  2elresin  5010  fnimadisj  5019  fco  5056  funssxp  5060  fssres  5066  feu  5072  fimacnvdisj  5074  fabexg  5077  f00  5081  f1co  5101  fores  5115  foco  5116  f1ores  5141  foimacnv  5144  f1oun  5146  fun11iun  5147  f1oco  5149  fo00  5162  brprcneu  5171  fv3  5197  relelfvdm  5205  nfvres  5206  nfunsn  5207  funfvbrb  5280  respreima  5295  dff2  5311  dff3im  5312  dffo4  5315  ffvresb  5328  f1oresrab  5329  fmptco  5330  fsn  5335  fpr  5345  ftpg  5347  fsnunf  5362  fsnunfv  5363  elabrex  5397  dff1o6  5416  foeqcnvco  5430  fliftel1  5434  isores1  5454  isoini2  5458  riotasbc  5483  acexmidlemph  5505  acexmidlemcase  5507  oprabidlem  5536  brabvv  5551  eloprabga  5591  fnoprabg  5602  caovimo  5694  oprabexd  5754  fo1stresm  5788  fo2ndresm  5789  unielxp  5800  1st2ndbr  5810  fmpt2co  5837  1stconst  5842  2ndconst  5843  poxp  5853  reldmtpos  5868  tposfun  5875  dftpos4  5878  smores  5907  smores2  5909  tfrlem1  5923  tfr0  5937  tfrlemibxssdm  5941  tfrlemibex  5943  tfrlemiubacc  5944  tfrlemi14d  5947  tfrexlem  5948  tfri1d  5949  tfri3  5953  2oconcl  6022  nnsucelsuc  6070  nntri3or  6072  nndceq  6077  nndcel  6078  nndifsnid  6080  ecexr  6111  brdifun  6133  ecelqsdm  6176  iinerm  6178  eroveu  6197  erovlem  6198  ecopovtrn  6203  ecopovtrng  6206  th3qlem1  6208  f1oen3g  6234  ssdomg  6258  domtr  6265  snfig  6291  php5dom  6325  fidceq  6330  fidifsnid  6332  nnfi  6333  fiunsnnn  6338  findcard  6345  findcard2  6346  findcard2s  6347  ac6sfi  6352  nnwetri  6354  dmaddpqlem  6475  nqpi  6476  dmaddpq  6477  dmmulpq  6478  ltdcnq  6495  subhalfnqq  6512  enq0sym  6530  enq0ref  6531  enq0tr  6532  nqnq0pi  6536  nq0nn  6540  addnq0mo  6545  mulnq0mo  6546  nqpnq0nq  6551  nqnq0a  6552  nqnq0m  6553  npsspw  6569  elnp1st2nd  6574  prnmaxl  6586  prnminu  6587  prarloc  6601  genprndl  6619  genprndu  6620  nqprm  6640  nqprl  6649  nqpru  6650  addnqprlemrl  6655  addnqprlemru  6656  prmuloc  6664  mulnqprlemrl  6671  mulnqprlemru  6672  ltsopr  6694  ltexprlemm  6698  ltexprlemopl  6699  ltexprlemopu  6701  lteupri  6715  recexprlemopl  6723  recexprlemopu  6725  recexprlemdisj  6728  archpr  6741  cauappcvgprlemdisj  6749  cauappcvgprlemladdrl  6755  cauappcvgprlem2  6758  caucvgprlemnbj  6765  caucvgprlemdisj  6772  caucvgprlemladdfu  6775  caucvgprlem2  6778  caucvgprprlemnbj  6791  caucvgprprlemdisj  6800  addsrmo  6828  mulsrmo  6829  recexgt0sr  6858  prsrpos  6869  caucvgsrlemasr  6874  elrealeu  6906  pitonn  6924  pitoregt0  6925  pitore  6926  recnnre  6927  axaddcl  6940  axaddrcl  6941  axmulcl  6942  axmulrcl  6943  axrnegex  6953  axcnre  6955  axpre-lttrn  6958  rereceu  6963  axarch  6965  ltxrlt  7085  apirr  7596  rerecclap  7706  arch  8178  0mnnnnn0  8214  nnm1nn0  8223  elnnnn0c  8227  elnnz1  8268  ztri3or0  8287  nn0n0n1ge2  8311  zdceq  8316  zdcle  8317  zdclt  8318  uzind  8349  eluzge3nn  8514  eluz2b2  8540  elnn1uz2  8544  nn01to3  8552  znq  8559  qaddcl  8570  qmulcl  8572  qreccl  8576  irradd  8580  irrmul  8581  cnref1o  8582  iooidg  8778  elioo4g  8803  fzdcel  8904  fznlem  8905  fzpreddisj  8933  elfz0ubfz0  8982  elfz0fzfz0  8983  fz0fzelfz0  8984  fz0fzdiffz0  8987  elfzmlbp  8990  difelfzle  8992  4fvwrd4  8997  fzosplit  9033  elfzo0  9038  fzo1fzo0n0  9039  elfzonn0  9042  fzofzim  9044  elfzo1  9046  elfzom1elp1fzo  9058  fzossfzop1  9068  ssfzo12bi  9081  qdceq  9102  qbtwnzlemstep  9103  qbtwnzlemex  9105  qbtwnz  9106  rebtwn2zlemstep  9107  rebtwn2z  9109  frec2uzrand  9191  frec2uzf1od  9192  frecuzrdgrom  9196  frecuzrdgfn  9198  frecfzennn  9203  iseqf  9224  iser0f  9251  expcl2lemap  9267  shftfvalg  9419  shftfval  9422  caucvgre  9580  rexanuz  9587  recvguniq  9593  rennim  9600  resqrexlemf  9605  rsqrmo  9625  climeu  9817  ialgrf  9884  algcvgblem  9888  bj-nfalt  9904  bj-indind  10056  bj-2inf  10062  peano5setOLD  10065  bj-nntrans2  10077  bj-peano4  10080  bj-nnord  10083  bj-inf2vn  10099  bj-inf2vn2  10100  bj-findis  10104