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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm5.63dc  959  sb1  1819  reurmo  2772  eldifn  3352  elinel2  3416  rabsnt  3786  eldifsni  3843  unimax  3969  ssintub  3988  exmidsssnc  4340  moop2  4392  wepo  4504  wetrep  4505  trssord  4525  ordelord  4526  ordsucim  4647  ordtri2or2exmidlem  4673  regexmidlem1  4680  reg2exmidlema  4681  tfis  4730  opelxp2  4809  funmo  5392  funopg  5411  funco  5417  funun  5422  fununi  5449  funimaexglem  5464  fndm  5480  frn  5542  f1ss  5604  f1ssr  5605  f1ssres  5607  forn  5618  f1f1orn  5650  f1orescnv  5655  f1imacnv  5656  funcocnv2  5664  funfveu  5708  nfvres  5732  isorel  6014  isoini2  6025  f1ofveu  6073  fovcld  6193  f1opw  6297  f1o2ndf1  6464  mpoxopn0yelv  6510  swoer  6835  mapsnconst  6976  en0  7082  en1  7086  phplem4  7156  phplem4dom  7163  phplem4on  7169  ssfilem  7177  ssfilemd  7179  diffitest  7191  inffiexmid  7213  fsuppcorn  7301  supubti  7339  suplubti  7340  djuinr  7403  casefun  7425  casef1  7430  djufun  7444  nnnninfeq  7468  ctssexmid  7490  exmidonfinlem  7545  exmidfodomrlemim  7553  cc4f  7635  cc4n  7637  0npi  7680  mulclpi  7695  mulcanpig  7702  nlt1pig  7708  indpi  7709  nnppipi  7710  dfplpq2  7721  archnqq  7784  enq0tr  7801  nqnq0pi  7805  ltexprlemopl  7968  ltexprlemopu  7970  cauappcvgprlemopl  8013  cauappcvgprlemlol  8014  cauappcvgprlemopu  8015  cauappcvgprlemupu  8016  cauappcvgprlemdisj  8018  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemopu  8038  caucvgprlemupu  8039  caucvgprlemdisj  8041  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemopu  8066  caucvgprprlemupu  8067  caucvgprprlemdisj  8069  suplocsrlempr  8174  ltresr2  8207  peano2nnnn  8220  axrnegex  8246  ltxrlt  8391  peano2nn  9317  elnn0z  9659  zaddcl  9686  ztri3or0  9688  eluz2gt1  10004  1nuz2  10008  rpgt0  10068  ixxss1  10308  ixxss2  10309  ixxss12  10310  iccss2  10348  iccssico2  10351  elfzuz3  10427  uzdisj  10502  nn0disj  10547  zsupcllemstep  10664  zsupssdc  10675  addmodlteq  10837  expge0  11014  expge1  11015  expaddzaplem  11021  shftfn  11591  fsumf1o  12159  fsumge0  12228  fprodf1o  12357  bitsfzolem  12723  bezoutlemzz  12781  bezoutlemaz  12782  bezoutlembz  12783  bezoutlemsup  12788  1nprm  12894  nprm  12903  sqnprm  12916  dvdsprm  12917  coprm  12924  sqpweven  12955  2sqpwodd  12956  dfphi2  13000  phimullem  13005  eulerthlemrprm  13009  phisum  13021  expnprm  13134  1arith  13148  4sqlem18  13189  ballotfilem4  13243  ballotfilem5  13244  ballotfilemfrc  13272  ballotfilemirc  13277  ballotfilemth  13283  oddennn  13285  znnen  13291  ennnfonelemg  13296  ctinf  13323  mndid  13740  mhmf  13774  mhmlin  13776  mhm0  13777  grpinvex  13817  grplinv  13857  mulgz  13955  mulgdirlem  13958  mulgdir  13959  mulgass  13964  nsgbi  14009  nmzbi  14014  ghmf  14052  ghmlin  14053  conjnsg  14086  ablcmn  14096  cmncom  14107  crngmgp  14310  rhmmhm  14468  rhmghm  14471  rimf1o  14479  nzrnz  14491  subrgss  14532  subrg1cl  14539  rrgeq0i  14574  domneq0  14583  fldcrngd  14618  2idlelbas  14855  2idlcpblrng  14862  znidomb  14995  assalem  15005  toponuni  15118  tpsuni  15137  neipsm  15257  cnf  15307  cnima  15323  txdis1cn  15381  hmeocnvcn  15409  psmetxrge0  15435  isxmet2d  15451  xmstopn  15558  mstopn  15559  bdxmet  15604  divcnap  15668  ivthinclemlr  15740  ivthinclemur  15742  dvlemap  15783  dvcnp2cntop  15802  dvaddxxbr  15804  dvmulxxbr  15805  dvcoapbr  15810  dvcjbr  15811  dvrecap  15816  dveflem  15829  plyf  15840  plyadd  15854  plymul  15855  plycn  15865  dvply2g  15869  dvdsppwf1o  16109  mpodvdsmulf1o  16110  lgsfle1  16140  lgsle1  16146  lgsdirprm  16165  lgsne0  16169  lgsquadlem1  16208  lgsquadlem2  16209  upgr1or2  16354  umgredg2en  16362  lfgredg2dom  16385  upgr2wlkdc  16630  trlres  16643  clwwlknon  16682  bj-indsuc  16966  nnsf  17060  als-no-surprise  17159  alseueu  17190