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  3netr4g  2237  necon3bi  2252  necon2ai  2256  alral  2364  rspe  2367  rsp2e  2369  rgen2a  2372  ralrimi  2387  r19.27av  2445  r19.32r  2454  nfreudxy  2480  mormo  2518  nrexrmo  2523  cgsex2g  2587  cgsex4g  2588  spc2egv  2639  spc2gv  2640  spc3egv  2641  spc3gv  2642  rspce  2648  ceqex  2668  elrab3t  2694  mosubt  2715  mo2icl  2717  reu3  2728  reu6i  2729  2rmorex  2742  sbc5  2784  rspesbca  2839  rmo2ilem  2844  sbnfc2  2903  ssrd  2947  ssrdv  2948  3sstr4g  2983  syl5eqss  2986  ss2abdv  3010  abssdv  3011  rabssdv  3017  ss2rabdv  3018  ssun1  3103  unssad  3117  unssbd  3118  ssddif  3168  uneqin  3185  indifdir  3190  undif3ss  3195  reuss2  3214  n0rf  3230  reximdva0m  3233  rabxmdc  3246  ssindif0im  3278  minel  3280  ralidm  3318  ralm  3322  disjsn2  3430  absneu  3439  rabsneu  3440  opprc  3567  elunii  3582  dfnfc2  3595  uniss2  3608  unidif  3609  ssunieq  3610  intab  3641  iunss2  3699  iunxdif2  3702  invdisj  3756  3brtr4g  3793  trin  3861  triun  3864  truni  3865  trint  3866  iinexgm  3905  class2seteq  3913  pwuni  3940  mss  3959  copsex2t  3979  euotd  3988  pwunim  4020  ispod  4038  sotricim  4057  exse  4070  trssord  4113  suctr  4154  eusvnf  4181  eusvnfb  4182  eusv2nf  4184  rexxfrd  4191  ralxfr2d  4192  rexxfr2d  4193  rabxfrd  4197  reuhypd  4199  eldifpw  4204  iunpw  4207  ssorduni  4209  sucelon  4225  onsucelsucr  4230  sucunielr  4232  ordtri2or2exmidlem  4247  onsucelsucexmid  4251  setindel  4257  elirr  4260  orddisj  4264  en2lp  4272  suc11g  4275  ordsuc  4281  nlimsucg  4284  onpsssuc  4289  ordtri2or2exmid  4290  tfi  4292  peano5  4308  limom  4323  peano2b  4324  nndceq0  4326  eqrelrdv  4423  xpsspw  4437  relint  4448  relop  4473  eqbrrdva  4492  opeldm  4525  elres  4633  relssres  4635  exse2  4686  issref  4694  trin2  4703  dminss  4725  imainss  4726  rnxpid  4742  dmsn0el  4777  dmmptg  4805  relrelss  4831  cnviinm  4846  iotanul  4869  sniota  4881  dffun5r  4901  funmo  4904  funco  4927  funun  4931  funprg  4936  funtpg  4937  funtp  4939  fntpg  4942  fununi  4954  funcnvuni  4955  imadiflem  4965  imainlem  4967  funimaexglem  4969  isarep2  4973  fnunsn  4993  2elresin  4997  fnimadisj  5006  fco  5043  funssxp  5047  fssres  5053  feu  5059  fimacnvdisj  5061  fabexg  5064  f00  5068  f1co  5088  fores  5102  foco  5103  f1ores  5128  foimacnv  5131  f1oun  5133  fun11iun  5134  f1oco  5136  fo00  5149  brprcneu  5158  fv3  5184  relelfvdm  5192  nfvres  5193  nfunsn  5194  funfvbrb  5267  respreima  5282  dff2  5298  dff3im  5299  dffo4  5302  ffvresb  5315  f1oresrab  5316  fmptco  5317  fsn  5322  fpr  5332  ftpg  5334  fsnunf  5349  fsnunfv  5350  elabrex  5384  dff1o6  5403  foeqcnvco  5417  fliftel1  5421  isores1  5441  isoini2  5445  riotasbc  5470  acexmidlemph  5492  acexmidlemcase  5494  oprabidlem  5523  brabvv  5538  eloprabga  5578  fnoprabg  5589  caovimo  5681  oprabexd  5741  fo1stresm  5775  fo2ndresm  5776  unielxp  5787  1st2ndbr  5797  fmpt2co  5824  1stconst  5829  2ndconst  5830  poxp  5840  reldmtpos  5855  tposfun  5862  dftpos4  5865  smores  5894  smores2  5896  tfrlem1  5910  tfr0  5924  tfrlemibxssdm  5928  tfrlemibex  5930  tfrlemiubacc  5931  tfrlemi14d  5934  tfrexlem  5935  tfri1d  5936  tfri3  5940  2oconcl  6009  nnsucelsuc  6057  nntri3or  6059  nndceq  6064  nndcel  6065  nndifsnid  6067  ecexr  6098  brdifun  6120  ecelqsdm  6163  iinerm  6165  eroveu  6184  erovlem  6185  ecopovtrn  6190  ecopovtrng  6193  th3qlem1  6195  f1oen3g  6221  ssdomg  6245  domtr  6252  snfig  6278  php5dom  6312  fidceq  6317  fidifsnid  6319  nnfi  6320  fiunsnnn  6325  findcard  6331  findcard2  6332  findcard2s  6333  ac6sfi  6338  dmaddpqlem  6456  nqpi  6457  dmaddpq  6458  dmmulpq  6459  ltdcnq  6476  subhalfnqq  6493  enq0sym  6511  enq0ref  6512  enq0tr  6513  nqnq0pi  6517  nq0nn  6521  addnq0mo  6526  mulnq0mo  6527  nqpnq0nq  6532  nqnq0a  6533  nqnq0m  6534  npsspw  6550  elnp1st2nd  6555  prnmaxl  6567  prnminu  6568  prarloc  6582  genprndl  6600  genprndu  6601  nqprm  6621  nqprl  6630  nqpru  6631  addnqprlemrl  6636  addnqprlemru  6637  prmuloc  6645  mulnqprlemrl  6652  mulnqprlemru  6653  ltsopr  6675  ltexprlemm  6679  ltexprlemopl  6680  ltexprlemopu  6682  lteupri  6696  recexprlemopl  6704  recexprlemopu  6706  recexprlemdisj  6709  archpr  6722  cauappcvgprlemdisj  6730  cauappcvgprlemladdrl  6736  cauappcvgprlem2  6739  caucvgprlemnbj  6746  caucvgprlemdisj  6753  caucvgprlemladdfu  6756  caucvgprlem2  6759  caucvgprprlemnbj  6772  caucvgprprlemdisj  6781  addsrmo  6809  mulsrmo  6810  recexgt0sr  6839  prsrpos  6850  caucvgsrlemasr  6855  elrealeu  6887  pitonn  6905  pitoregt0  6906  pitore  6907  recnnre  6908  axaddcl  6921  axaddrcl  6922  axmulcl  6923  axmulrcl  6924  axrnegex  6934  axcnre  6936  axpre-lttrn  6939  rereceu  6944  axarch  6946  ltxrlt  7065  apirr  7572  rerecclap  7682  arch  8150  0mnnnnn0  8186  nnm1nn0  8195  elnnnn0c  8199  elnnz1  8240  ztri3or0  8259  nn0n0n1ge2  8283  zdceq  8288  zdcle  8289  zdclt  8290  uzind  8321  eluzge3nn  8486  eluz2b2  8512  elnn1uz2  8516  nn01to3  8524  znq  8531  qaddcl  8542  qmulcl  8544  qreccl  8547  irradd  8551  irrmul  8552  cnref1o  8553  iooidg  8745  elioo4g  8770  fzdcel  8871  fznlem  8872  fzpreddisj  8900  elfz0ubfz0  8949  elfz0fzfz0  8950  fz0fzelfz0  8951  fz0fzdiffz0  8954  elfzmlbp  8957  difelfzle  8959  4fvwrd4  8964  fzosplit  9000  elfzo0  9005  fzo1fzo0n0  9006  elfzonn0  9009  fzofzim  9011  elfzo1  9013  elfzom1elp1fzo  9025  fzossfzop1  9035  ssfzo12bi  9048  frec2uzrand  9069  frec2uzf1od  9070  frecuzrdgrom  9074  frecuzrdgfn  9076  frecfzennn  9081  iseqf  9102  iser0f  9129  expcl2lemap  9145  shftfvalg  9297  shftfval  9300  caucvgre  9458  rexanuz  9465  recvguniq  9471  rennim  9478  resqrexlemf  9483  rsqrmo  9503  climeu  9694  ialgrf  9761  algcvgblem  9765  bj-nfalt  9777  bj-indind  9929  bj-2inf  9935  peano5setOLD  9938  bj-nntrans2  9950  bj-peano4  9953  bj-nnord  9956  bj-inf2vn  9972  bj-inf2vn2  9973  bj-findis  9977