Theorem simprbi 275

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 120	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 114	1 ⊢ (𝜑 → 𝜒)

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.63dc  955  sb1  1815  reurmo  2766  eldifn  3346  elinel2  3410  rabsnt  3771  eldifsni  3827  unimax  3953  ssintub  3972  exmidsssnc  4321  moop2  4373  wepo  4485  wetrep  4486  trssord  4506  ordelord  4507  ordsucim  4627  ordtri2or2exmidlem  4653  regexmidlem1  4660  reg2exmidlema  4661  tfis  4710  opelxp2  4789  funmo  5372  funopg  5391  funco  5397  funun  5402  fununi  5429  funimaexglem  5444  fndm  5460  frn  5522  f1ss  5584  f1ssr  5585  f1ssres  5587  forn  5598  f1f1orn  5630  f1orescnv  5635  f1imacnv  5636  funcocnv2  5644  funfveu  5688  nfvres  5711  isorel  5987  isoini2  5998  f1ofveu  6046  fovcld  6166  f1opw  6270  f1o2ndf1  6437  mpoxopn0yelv  6483  swoer  6808  mapsnconst  6942  en0  7048  en1  7052  phplem4  7122  phplem4dom  7129  phplem4on  7135  ssfilem  7143  ssfilemd  7145  diffitest  7157  inffiexmid  7179  fsuppcorn  7267  supubti  7303  suplubti  7304  djuinr  7367  casefun  7389  casef1  7394  djufun  7408  nnnninfeq  7432  ctssexmid  7454  exmidonfinlem  7509  exmidfodomrlemim  7517  cc4f  7599  cc4n  7601  0npi  7644  mulclpi  7659  mulcanpig  7666  nlt1pig  7672  indpi  7673  nnppipi  7674  dfplpq2  7685  archnqq  7748  enq0tr  7765  nqnq0pi  7769  ltexprlemopl  7932  ltexprlemopu  7934  cauappcvgprlemopl  7977  cauappcvgprlemlol  7978  cauappcvgprlemopu  7979  cauappcvgprlemupu  7980  cauappcvgprlemdisj  7982  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemopu  8002  caucvgprlemupu  8003  caucvgprlemdisj  8005  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemopu  8030  caucvgprprlemupu  8031  caucvgprprlemdisj  8033  suplocsrlempr  8138  ltresr2  8171  peano2nnnn  8184  axrnegex  8210  ltxrlt  8355  peano2nn  9269  elnn0z  9610  zaddcl  9637  ztri3or0  9639  eluz2gt1  9955  1nuz2  9959  rpgt0  10019  ixxss1  10259  ixxss2  10260  ixxss12  10261  iccss2  10299  iccssico2  10302  elfzuz3  10378  uzdisj  10452  nn0disj  10497  zsupcllemstep  10614  zsupssdc  10625  addmodlteq  10787  expge0  10964  expge1  10965  expaddzaplem  10971  shftfn  11537  fsumf1o  12104  fsumge0  12173  fprodf1o  12302  bitsfzolem  12668  bezoutlemzz  12726  bezoutlemaz  12727  bezoutlembz  12728  bezoutlemsup  12733  1nprm  12839  nprm  12848  sqnprm  12861  dvdsprm  12862  coprm  12869  sqpweven  12900  2sqpwodd  12901  dfphi2  12945  phimullem  12950  eulerthlemrprm  12954  phisum  12966  expnprm  13079  1arith  13093  4sqlem18  13134  ballotfilem4  13188  ballotfilem5  13189  ballotfilemfrc  13217  ballotfilemirc  13222  ballotfilemth  13228  oddennn  13230  znnen  13236  ennnfonelemg  13241  ctinf  13268  mndid  13689  mhmf  13723  mhmlin  13725  mhm0  13726  grpinvex  13768  grplinv  13808  mulgz  13906  mulgdirlem  13909  mulgdir  13910  mulgass  13915  nsgbi  13960  nmzbi  13965  ghmf  14003  ghmlin  14004  conjnsg  14037  ablcmn  14047  cmncom  14058  crngmgp  14250  rhmmhm  14407  rhmghm  14410  rimf1o  14418  nzrnz  14430  subrgss  14471  subrg1cl  14478  rrgeq0i  14513  domneq0  14522  fldcrngd  14557  2idlelbas  14793  2idlcpblrng  14800  znidomb  14935  toponuni  15009  tpsuni  15028  neipsm  15148  cnf  15198  cnima  15214  txdis1cn  15272  hmeocnvcn  15300  psmetxrge0  15326  isxmet2d  15342  xmstopn  15449  mstopn  15450  bdxmet  15495  divcnap  15559  ivthinclemlr  15631  ivthinclemur  15633  dvlemap  15674  dvcnp2cntop  15693  dvaddxxbr  15695  dvmulxxbr  15696  dvcoapbr  15701  dvcjbr  15702  dvrecap  15707  dveflem  15720  plyf  15731  plyadd  15745  plymul  15746  plycn  15756  dvply2g  15760  dvdsppwf1o  15986  mpodvdsmulf1o  15987  lgsfle1  16011  lgsle1  16017  lgsdirprm  16036  lgsne0  16040  lgsquadlem1  16079  lgsquadlem2  16080  upgr1or2  16225  umgredg2en  16233  lfgredg2dom  16256  upgr2wlkdc  16501  trlres  16514  clwwlknon  16553  bj-indsuc  16837  nnsf  16922