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  951  sb1  1792  reurmo  2731  eldifn  3307  elinel2  3371  rabsnt  3721  eldifsni  3776  unimax  3901  ssintub  3920  exmidsssnc  4266  moop2  4317  wepo  4427  wetrep  4428  trssord  4448  ordelord  4449  ordsucim  4569  ordtri2or2exmidlem  4595  regexmidlem1  4602  reg2exmidlema  4603  tfis  4652  opelxp2  4731  funmo  5309  funopg  5328  funco  5334  funun  5338  fununi  5365  funimaexglem  5380  fndm  5396  frn  5458  f1ss  5513  f1ssr  5514  f1ssres  5516  forn  5527  f1f1orn  5559  f1orescnv  5564  f1imacnv  5565  funcocnv2  5573  funfveu  5616  nfvres  5637  isorel  5905  isoini2  5916  f1ofveu  5962  fovcld  6080  f1opw  6183  f1o2ndf1  6344  mpoxopn0yelv  6355  swoer  6678  mapsnconst  6811  en0  6917  en1  6921  phplem4  6984  phplem4dom  6991  phplem4on  6997  ssfilem  7005  diffitest  7017  inffiexmid  7036  supubti  7134  suplubti  7135  djuinr  7198  casefun  7220  casef1  7225  djufun  7239  nnnninfeq  7263  ctssexmid  7285  exmidonfinlem  7339  exmidfodomrlemim  7347  cc4f  7423  cc4n  7425  0npi  7468  mulclpi  7483  mulcanpig  7490  nlt1pig  7496  indpi  7497  nnppipi  7498  dfplpq2  7509  archnqq  7572  enq0tr  7589  nqnq0pi  7593  ltexprlemopl  7756  ltexprlemopu  7758  cauappcvgprlemopl  7801  cauappcvgprlemlol  7802  cauappcvgprlemopu  7803  cauappcvgprlemupu  7804  cauappcvgprlemdisj  7806  caucvgprlemopl  7824  caucvgprlemlol  7825  caucvgprlemopu  7826  caucvgprlemupu  7827  caucvgprlemdisj  7829  caucvgprprlemopl  7852  caucvgprprlemlol  7853  caucvgprprlemopu  7854  caucvgprprlemupu  7855  caucvgprprlemdisj  7857  suplocsrlempr  7962  ltresr2  7995  peano2nnnn  8008  axrnegex  8034  ltxrlt  8180  peano2nn  9090  elnn0z  9427  zaddcl  9454  ztri3or0  9456  eluz2gt1  9765  1nuz2  9769  rpgt0  9829  ixxss1  10068  ixxss2  10069  ixxss12  10070  iccss2  10108  iccssico2  10111  elfzuz3  10186  uzdisj  10257  nn0disj  10302  zsupcllemstep  10416  zsupssdc  10425  addmodlteq  10587  expge0  10764  expge1  10765  expaddzaplem  10771  shftfn  11301  fsumf1o  11867  fsumge0  11936  fprodf1o  12065  bitsfzolem  12431  bezoutlemzz  12489  bezoutlemaz  12490  bezoutlembz  12491  bezoutlemsup  12496  1nprm  12602  nprm  12611  sqnprm  12624  dvdsprm  12625  coprm  12632  sqpweven  12663  2sqpwodd  12664  dfphi2  12708  phimullem  12713  eulerthlemrprm  12717  phisum  12729  expnprm  12842  1arith  12856  4sqlem18  12897  oddennn  12929  znnen  12935  ennnfonelemg  12940  ctinf  12967  mndid  13424  mhmf  13464  mhmlin  13466  mhm0  13467  grpinvex  13509  grplinv  13549  mulgz  13653  mulgdirlem  13656  mulgdir  13657  mulgass  13662  nsgbi  13707  nmzbi  13712  ghmf  13750  ghmlin  13751  conjnsg  13784  ablcmn  13794  cmncom  13805  crngmgp  13933  rhmmhm  14088  rhmghm  14091  rimf1o  14099  nzrnz  14111  subrgss  14151  subrg1cl  14158  rrgeq0i  14193  domneq0  14201  2idlelbas  14445  2idlcpblrng  14452  znidomb  14587  toponuni  14654  tpsuni  14673  neipsm  14793  cnf  14843  cnima  14859  txdis1cn  14917  hmeocnvcn  14945  psmetxrge0  14971  isxmet2d  14987  xmstopn  15094  mstopn  15095  bdxmet  15140  divcnap  15204  ivthinclemlr  15276  ivthinclemur  15278  dvlemap  15319  dvcnp2cntop  15338  dvaddxxbr  15340  dvmulxxbr  15341  dvcoapbr  15346  dvcjbr  15347  dvrecap  15352  dveflem  15365  plyf  15376  plyadd  15390  plymul  15391  plycn  15401  dvply2g  15405  dvdsppwf1o  15628  mpodvdsmulf1o  15629  lgsfle1  15653  lgsle1  15659  lgsdirprm  15678  lgsne0  15682  lgsquadlem1  15721  lgsquadlem2  15722  upgr1or2  15866  umgredg2en  15874  lfgredg2dom  15895  bj-indsuc  16201  nnsf  16282