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  954  sb1  1814  reurmo  2753  eldifn  3330  elinel2  3394  rabsnt  3746  eldifsni  3802  unimax  3927  ssintub  3946  exmidsssnc  4293  moop2  4344  wepo  4456  wetrep  4457  trssord  4477  ordelord  4478  ordsucim  4598  ordtri2or2exmidlem  4624  regexmidlem1  4631  reg2exmidlema  4632  tfis  4681  opelxp2  4760  funmo  5341  funopg  5360  funco  5366  funun  5371  fununi  5398  funimaexglem  5413  fndm  5429  frn  5491  f1ss  5548  f1ssr  5549  f1ssres  5551  forn  5562  f1f1orn  5594  f1orescnv  5599  f1imacnv  5600  funcocnv2  5608  funfveu  5652  nfvres  5675  isorel  5949  isoini2  5960  f1ofveu  6006  fovcld  6126  f1opw  6230  f1o2ndf1  6393  mpoxopn0yelv  6405  swoer  6730  mapsnconst  6863  en0  6969  en1  6973  phplem4  7041  phplem4dom  7048  phplem4on  7054  ssfilem  7062  ssfilemd  7064  diffitest  7076  inffiexmid  7098  supubti  7198  suplubti  7199  djuinr  7262  casefun  7284  casef1  7289  djufun  7303  nnnninfeq  7327  ctssexmid  7349  exmidonfinlem  7404  exmidfodomrlemim  7412  cc4f  7488  cc4n  7490  0npi  7533  mulclpi  7548  mulcanpig  7555  nlt1pig  7561  indpi  7562  nnppipi  7563  dfplpq2  7574  archnqq  7637  enq0tr  7654  nqnq0pi  7658  ltexprlemopl  7821  ltexprlemopu  7823  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemopu  7868  cauappcvgprlemupu  7869  cauappcvgprlemdisj  7871  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemopu  7891  caucvgprlemupu  7892  caucvgprlemdisj  7894  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemupu  7920  caucvgprprlemdisj  7922  suplocsrlempr  8027  ltresr2  8060  peano2nnnn  8073  axrnegex  8099  ltxrlt  8245  peano2nn  9155  elnn0z  9492  zaddcl  9519  ztri3or0  9521  eluz2gt1  9836  1nuz2  9840  rpgt0  9900  ixxss1  10139  ixxss2  10140  ixxss12  10141  iccss2  10179  iccssico2  10182  elfzuz3  10257  uzdisj  10328  nn0disj  10373  zsupcllemstep  10490  zsupssdc  10499  addmodlteq  10661  expge0  10838  expge1  10839  expaddzaplem  10845  shftfn  11386  fsumf1o  11953  fsumge0  12022  fprodf1o  12151  bitsfzolem  12517  bezoutlemzz  12575  bezoutlemaz  12576  bezoutlembz  12577  bezoutlemsup  12582  1nprm  12688  nprm  12697  sqnprm  12710  dvdsprm  12711  coprm  12718  sqpweven  12749  2sqpwodd  12750  dfphi2  12794  phimullem  12799  eulerthlemrprm  12803  phisum  12815  expnprm  12928  1arith  12942  4sqlem18  12983  oddennn  13015  znnen  13021  ennnfonelemg  13026  ctinf  13053  mndid  13510  mhmf  13550  mhmlin  13552  mhm0  13553  grpinvex  13595  grplinv  13635  mulgz  13739  mulgdirlem  13742  mulgdir  13743  mulgass  13748  nsgbi  13793  nmzbi  13798  ghmf  13836  ghmlin  13837  conjnsg  13870  ablcmn  13880  cmncom  13891  crngmgp  14020  rhmmhm  14176  rhmghm  14179  rimf1o  14187  nzrnz  14199  subrgss  14239  subrg1cl  14246  rrgeq0i  14281  domneq0  14289  2idlelbas  14533  2idlcpblrng  14540  znidomb  14675  toponuni  14742  tpsuni  14761  neipsm  14881  cnf  14931  cnima  14947  txdis1cn  15005  hmeocnvcn  15033  psmetxrge0  15059  isxmet2d  15075  xmstopn  15182  mstopn  15183  bdxmet  15228  divcnap  15292  ivthinclemlr  15364  ivthinclemur  15366  dvlemap  15407  dvcnp2cntop  15426  dvaddxxbr  15428  dvmulxxbr  15429  dvcoapbr  15434  dvcjbr  15435  dvrecap  15440  dveflem  15453  plyf  15464  plyadd  15478  plymul  15479  plycn  15489  dvply2g  15493  dvdsppwf1o  15716  mpodvdsmulf1o  15717  lgsfle1  15741  lgsle1  15747  lgsdirprm  15766  lgsne0  15770  lgsquadlem1  15809  lgsquadlem2  15810  upgr1or2  15955  umgredg2en  15963  lfgredg2dom  15986  upgr2wlkdc  16231  trlres  16244  clwwlknon  16283  bj-indsuc  16544  nnsf  16628