Theorem simprbi 273

Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)

Hypothesis

Ref	Expression
simprbi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simprbi	⊢ (𝜑 → 𝜒)

Proof of Theorem simprbi

Step	Hyp	Ref	Expression
1		simprbi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	biimpi 119	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 113	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.63dc  936  sb1  1754  reurmo  2679  eldifn  3244  elinel2  3308  rabsnt  3650  eldifsni  3704  unimax  3822  ssintub  3841  exmidsssnc  4181  moop2  4228  wepo  4336  wetrep  4337  trssord  4357  ordelord  4358  ordsucim  4476  ordtri2or2exmidlem  4502  regexmidlem1  4509  reg2exmidlema  4510  tfis  4559  opelxp2  4638  funmo  5202  funopg  5221  funco  5227  funun  5231  fununi  5255  funimaexglem  5270  fndm  5286  frn  5345  f1ss  5398  f1ssr  5399  f1ssres  5401  forn  5412  f1f1orn  5442  f1orescnv  5447  f1imacnv  5448  funcocnv2  5456  funfveu  5498  nfvres  5518  isorel  5775  isoini2  5786  f1ofveu  5829  fovcl  5943  f1opw  6044  f1o2ndf1  6192  mpoxopn0yelv  6203  swoer  6525  mapsnconst  6656  en0  6757  en1  6761  phplem4  6817  phplem4dom  6824  phplem4on  6829  ssfilem  6837  diffitest  6849  inffiexmid  6868  supubti  6960  suplubti  6961  djuinr  7024  casefun  7046  casef1  7051  djufun  7065  nnnninfeq  7088  ctssexmid  7110  exmidonfinlem  7145  exmidfodomrlemim  7153  cc4f  7206  cc4n  7208  0npi  7250  mulclpi  7265  mulcanpig  7272  nlt1pig  7278  indpi  7279  nnppipi  7280  dfplpq2  7291  archnqq  7354  enq0tr  7371  nqnq0pi  7375  ltexprlemopl  7538  ltexprlemopu  7540  cauappcvgprlemopl  7583  cauappcvgprlemlol  7584  cauappcvgprlemopu  7585  cauappcvgprlemupu  7586  cauappcvgprlemdisj  7588  caucvgprlemopl  7606  caucvgprlemlol  7607  caucvgprlemopu  7608  caucvgprlemupu  7609  caucvgprlemdisj  7611  caucvgprprlemopl  7634  caucvgprprlemlol  7635  caucvgprprlemopu  7636  caucvgprprlemupu  7637  caucvgprprlemdisj  7639  suplocsrlempr  7744  ltresr2  7777  peano2nnnn  7790  axrnegex  7816  ltxrlt  7960  peano2nn  8865  elnn0z  9200  zaddcl  9227  ztri3or0  9229  eluz2gt1  9536  1nuz2  9540  rpgt0  9597  ixxss1  9836  ixxss2  9837  ixxss12  9838  iccss2  9876  iccssico2  9879  elfzuz3  9953  uzdisj  10024  nn0disj  10069  addmodlteq  10329  expge0  10487  expge1  10488  expaddzaplem  10494  shftfn  10762  fsumf1o  11327  fsumge0  11396  fprodf1o  11525  zsupcllemstep  11874  zsupssdc  11883  bezoutlemzz  11931  bezoutlemaz  11932  bezoutlembz  11933  bezoutlemsup  11938  1nprm  12042  nprm  12051  sqnprm  12064  dvdsprm  12065  coprm  12072  sqpweven  12103  2sqpwodd  12104  dfphi2  12148  phimullem  12153  eulerthlemrprm  12157  phisum  12168  expnprm  12279  1arith  12293  oddennn  12321  znnen  12327  ennnfonelemg  12332  ctinf  12359  toponuni  12613  tpsuni  12632  neipsm  12754  cnf  12804  cnima  12820  txdis1cn  12878  hmeocnvcn  12906  psmetxrge0  12932  isxmet2d  12948  xmstopn  13055  mstopn  13056  bdxmet  13101  divcnap  13155  ivthinclemlr  13215  ivthinclemur  13217  dvlemap  13249  dvcnp2cntop  13263  dvaddxxbr  13265  dvmulxxbr  13266  dvcoapbr  13271  dvcjbr  13272  dvrecap  13277  dveflem  13287  lgsfle1  13510  lgsle1  13516  lgsdirprm  13535  lgsne0  13539  bj-indsuc  13770  nnsf  13845