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  959  sb1  1819  reurmo  2772  eldifn  3352  elinel2  3416  rabsnt  3785  eldifsni  3841  unimax  3967  ssintub  3986  exmidsssnc  4338  moop2  4390  wepo  4502  wetrep  4503  trssord  4523  ordelord  4524  ordsucim  4645  ordtri2or2exmidlem  4671  regexmidlem1  4678  reg2exmidlema  4679  tfis  4728  opelxp2  4807  funmo  5390  funopg  5409  funco  5415  funun  5420  fununi  5447  funimaexglem  5462  fndm  5478  frn  5540  f1ss  5602  f1ssr  5603  f1ssres  5605  forn  5616  f1f1orn  5648  f1orescnv  5653  f1imacnv  5654  funcocnv2  5662  funfveu  5706  nfvres  5729  isorel  6008  isoini2  6019  f1ofveu  6067  fovcld  6187  f1opw  6291  f1o2ndf1  6458  mpoxopn0yelv  6504  swoer  6829  mapsnconst  6970  en0  7076  en1  7080  phplem4  7150  phplem4dom  7157  phplem4on  7163  ssfilem  7171  ssfilemd  7173  diffitest  7185  inffiexmid  7207  fsuppcorn  7295  supubti  7333  suplubti  7334  djuinr  7397  casefun  7419  casef1  7424  djufun  7438  nnnninfeq  7462  ctssexmid  7484  exmidonfinlem  7539  exmidfodomrlemim  7547  cc4f  7629  cc4n  7631  0npi  7674  mulclpi  7689  mulcanpig  7696  nlt1pig  7702  indpi  7703  nnppipi  7704  dfplpq2  7715  archnqq  7778  enq0tr  7795  nqnq0pi  7799  ltexprlemopl  7962  ltexprlemopu  7964  cauappcvgprlemopl  8007  cauappcvgprlemlol  8008  cauappcvgprlemopu  8009  cauappcvgprlemupu  8010  cauappcvgprlemdisj  8012  caucvgprlemopl  8030  caucvgprlemlol  8031  caucvgprlemopu  8032  caucvgprlemupu  8033  caucvgprlemdisj  8035  caucvgprprlemopl  8058  caucvgprprlemlol  8059  caucvgprprlemopu  8060  caucvgprprlemupu  8061  caucvgprprlemdisj  8063  suplocsrlempr  8168  ltresr2  8201  peano2nnnn  8214  axrnegex  8240  ltxrlt  8385  peano2nn  9299  elnn0z  9640  zaddcl  9667  ztri3or0  9669  eluz2gt1  9985  1nuz2  9989  rpgt0  10049  ixxss1  10289  ixxss2  10290  ixxss12  10291  iccss2  10329  iccssico2  10332  elfzuz3  10408  uzdisj  10483  nn0disj  10528  zsupcllemstep  10645  zsupssdc  10656  addmodlteq  10818  expge0  10995  expge1  10996  expaddzaplem  11002  shftfn  11572  fsumf1o  12140  fsumge0  12209  fprodf1o  12338  bitsfzolem  12704  bezoutlemzz  12762  bezoutlemaz  12763  bezoutlembz  12764  bezoutlemsup  12769  1nprm  12875  nprm  12884  sqnprm  12897  dvdsprm  12898  coprm  12905  sqpweven  12936  2sqpwodd  12937  dfphi2  12981  phimullem  12986  eulerthlemrprm  12990  phisum  13002  expnprm  13115  1arith  13129  4sqlem18  13170  ballotfilem4  13224  ballotfilem5  13225  ballotfilemfrc  13253  ballotfilemirc  13258  ballotfilemth  13264  oddennn  13266  znnen  13272  ennnfonelemg  13277  ctinf  13304  mndid  13721  mhmf  13755  mhmlin  13757  mhm0  13758  grpinvex  13798  grplinv  13838  mulgz  13936  mulgdirlem  13939  mulgdir  13940  mulgass  13945  nsgbi  13990  nmzbi  13995  ghmf  14033  ghmlin  14034  conjnsg  14067  ablcmn  14077  cmncom  14088  crngmgp  14291  rhmmhm  14449  rhmghm  14452  rimf1o  14460  nzrnz  14472  subrgss  14513  subrg1cl  14520  rrgeq0i  14555  domneq0  14564  fldcrngd  14599  2idlelbas  14836  2idlcpblrng  14843  znidomb  14976  assalem  14986  toponuni  15099  tpsuni  15118  neipsm  15238  cnf  15288  cnima  15304  txdis1cn  15362  hmeocnvcn  15390  psmetxrge0  15416  isxmet2d  15432  xmstopn  15539  mstopn  15540  bdxmet  15585  divcnap  15649  ivthinclemlr  15721  ivthinclemur  15723  dvlemap  15764  dvcnp2cntop  15783  dvaddxxbr  15785  dvmulxxbr  15786  dvcoapbr  15791  dvcjbr  15792  dvrecap  15797  dveflem  15810  plyf  15821  plyadd  15835  plymul  15836  plycn  15846  dvply2g  15850  dvdsppwf1o  16086  mpodvdsmulf1o  16087  lgsfle1  16111  lgsle1  16117  lgsdirprm  16136  lgsne0  16140  lgsquadlem1  16179  lgsquadlem2  16180  upgr1or2  16325  umgredg2en  16333  lfgredg2dom  16356  upgr2wlkdc  16601  trlres  16614  clwwlknon  16653  bj-indsuc  16937  nnsf  17022  als-no-surprise  17121