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  4342  moop2  4394  wepo  4506  wetrep  4507  trssord  4527  ordelord  4528  ordsucim  4649  ordtri2or2exmidlem  4675  regexmidlem1  4682  reg2exmidlema  4683  tfis  4732  opelxp2  4811  funmo  5395  funopg  5414  funco  5420  funun  5425  fununi  5452  funimaexglem  5467  fndm  5483  frn  5545  f1ss  5607  f1ssr  5608  f1ssres  5610  forn  5621  f1f1orn  5653  f1orescnv  5658  f1imacnv  5659  funcocnv2  5667  funfveu  5711  nfvres  5735  isorel  6017  isoini2  6028  f1ofveu  6076  fovcld  6196  f1opw  6300  f1o2ndf1  6468  mpoxopn0yelv  6514  swoer  6839  mapsnconst  6981  en0  7087  en1  7091  phplem4  7161  phplem4dom  7168  phplem4on  7174  ssfilem  7182  ssfilemd  7184  diffitest  7196  inffiexmid  7218  fsuppcorn  7307  supubti  7346  suplubti  7347  djuinr  7410  casefun  7432  casef1  7437  djufun  7451  nnnninfeq  7475  ctssexmid  7497  exmidonfinlem  7552  exmidfodomrlemim  7560  cc4f  7642  cc4n  7644  0npi  7687  mulclpi  7702  mulcanpig  7709  nlt1pig  7715  indpi  7716  nnppipi  7717  dfplpq2  7728  archnqq  7791  enq0tr  7808  nqnq0pi  7812  ltexprlemopl  7975  ltexprlemopu  7977  cauappcvgprlemopl  8020  cauappcvgprlemlol  8021  cauappcvgprlemopu  8022  cauappcvgprlemupu  8023  cauappcvgprlemdisj  8025  caucvgprlemopl  8043  caucvgprlemlol  8044  caucvgprlemopu  8045  caucvgprlemupu  8046  caucvgprlemdisj  8048  caucvgprprlemopl  8071  caucvgprprlemlol  8072  caucvgprprlemopu  8073  caucvgprprlemupu  8074  caucvgprprlemdisj  8076  suplocsrlempr  8181  ltresr2  8214  peano2nnnn  8227  axrnegex  8253  ltxrlt  8398  peano2nn  9326  elnn0z  9669  zaddcl  9696  ztri3or0  9698  eluz2gt1  10019  1nuz2  10023  rpgt0  10084  ixxss1  10324  ixxss2  10325  ixxss12  10326  iccss2  10364  iccssico2  10367  elfzuz3  10443  uzdisj  10518  nn0disj  10563  zsupcllemstep  10680  zsupssdc  10691  addmodlteq  10857  expge0  11034  expge1  11035  expaddzaplem  11041  shftfn  11612  fsumf1o  12183  fsumge0  12252  fprodf1o  12381  bitsfzolem  12747  bezoutlemzz  12805  bezoutlemaz  12806  bezoutlembz  12807  bezoutlemsup  12812  1nprm  12918  nprm  12927  sqnprm  12941  dvdsprm  12942  coprm  12949  sqpweven  12981  2sqpwodd  12982  dfphi2  13028  phimullem  13033  eulerthlemrprm  13037  phisum  13049  expnprm  13162  1arith  13176  4sqlem18  13217  ballotfilem4  13300  ballotfilem5  13301  ballotfilemfrc  13329  ballotfilemirc  13334  ballotfilemth  13340  oddennn  13342  znnen  13348  ennnfonelemg  13353  ctinf  13380  mndid  13798  mhmf  13832  mhmlin  13834  mhm0  13835  grpinvex  13875  grplinv  13915  mulgz  14013  mulgdirlem  14016  mulgdir  14017  mulgass  14022  nsgbi  14067  nmzbi  14072  ghmf  14110  ghmlin  14111  conjnsg  14144  ablcmn  14185  cmncom  14196  crngmgp  14416  rhmmhm  14576  rhmghm  14579  rimf1o  14587  nzrnz  14599  subrgss  14640  subrg1cl  14647  rrgeq0i  14682  domneq0  14691  fldcrngd  14726  2idlelbas  14963  2idlcpblrng  14970  znidomb  15103  assalem  15113  rhmpsrfilem2  15190  toponuni  15253  tpsuni  15272  neipsm  15392  cnf  15442  cnima  15458  txdis1cn  15516  hmeocnvcn  15544  psmetxrge0  15570  isxmet2d  15586  xmstopn  15693  mstopn  15694  bdxmet  15739  divcnap  15803  ivthinclemlr  15875  ivthinclemur  15877  dvlemap  15918  dvcnp2cntop  15937  dvaddxxbr  15939  dvmulxxbr  15940  dvcoapbr  15945  dvcjbr  15946  dvrecap  15951  dveflem  15964  plyf  15975  plyadd  15989  plymul  15990  plycn  16000  dvply2g  16004  efnnfsumcl  16251  efchtqdvds  16277  dvdsppwf1o  16295  mpodvdsmulf1o  16296  lgsfle1  16345  lgsle1  16351  lgsdirprm  16370  lgsne0  16374  lgsquadlem1  16413  lgsquadlem2  16414  upgr1or2  16559  umgredg2en  16567  lfgredg2dom  16590  upgr2wlkdc  16835  trlres  16848  clwwlknon  16887  bj-indsuc  17171  nnsf  17266  als-no-surprise  17366  alseueu  17397