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  955  sb1  1815  reurmo  2766  eldifn  3344  elinel2  3408  rabsnt  3768  eldifsni  3824  unimax  3950  ssintub  3969  exmidsssnc  4318  moop2  4370  wepo  4482  wetrep  4483  trssord  4503  ordelord  4504  ordsucim  4624  ordtri2or2exmidlem  4650  regexmidlem1  4657  reg2exmidlema  4658  tfis  4707  opelxp2  4786  funmo  5369  funopg  5388  funco  5394  funun  5399  fununi  5426  funimaexglem  5441  fndm  5457  frn  5519  f1ss  5581  f1ssr  5582  f1ssres  5584  forn  5595  f1f1orn  5627  f1orescnv  5632  f1imacnv  5633  funcocnv2  5641  funfveu  5685  nfvres  5708  isorel  5983  isoini2  5994  f1ofveu  6040  fovcld  6160  f1opw  6264  f1o2ndf1  6426  mpoxopn0yelv  6472  swoer  6797  mapsnconst  6931  en0  7037  en1  7041  phplem4  7111  phplem4dom  7118  phplem4on  7124  ssfilem  7132  ssfilemd  7134  diffitest  7146  inffiexmid  7168  fsuppcorn  7256  supubti  7292  suplubti  7293  djuinr  7356  casefun  7378  casef1  7383  djufun  7397  nnnninfeq  7421  ctssexmid  7443  exmidonfinlem  7498  exmidfodomrlemim  7506  cc4f  7588  cc4n  7590  0npi  7633  mulclpi  7648  mulcanpig  7655  nlt1pig  7661  indpi  7662  nnppipi  7663  dfplpq2  7674  archnqq  7737  enq0tr  7754  nqnq0pi  7758  ltexprlemopl  7921  ltexprlemopu  7923  cauappcvgprlemopl  7966  cauappcvgprlemlol  7967  cauappcvgprlemopu  7968  cauappcvgprlemupu  7969  cauappcvgprlemdisj  7971  caucvgprlemopl  7989  caucvgprlemlol  7990  caucvgprlemopu  7991  caucvgprlemupu  7992  caucvgprlemdisj  7994  caucvgprprlemopl  8017  caucvgprprlemlol  8018  caucvgprprlemopu  8019  caucvgprprlemupu  8020  caucvgprprlemdisj  8022  suplocsrlempr  8127  ltresr2  8160  peano2nnnn  8173  axrnegex  8199  ltxrlt  8344  peano2nn  9254  elnn0z  9595  zaddcl  9622  ztri3or0  9624  eluz2gt1  9940  1nuz2  9944  rpgt0  10004  ixxss1  10243  ixxss2  10244  ixxss12  10245  iccss2  10283  iccssico2  10286  elfzuz3  10362  uzdisj  10434  nn0disj  10479  zsupcllemstep  10596  zsupssdc  10605  addmodlteq  10767  expge0  10944  expge1  10945  expaddzaplem  10951  shftfn  11517  fsumf1o  12084  fsumge0  12153  fprodf1o  12282  bitsfzolem  12648  bezoutlemzz  12706  bezoutlemaz  12707  bezoutlembz  12708  bezoutlemsup  12713  1nprm  12819  nprm  12828  sqnprm  12841  dvdsprm  12842  coprm  12849  sqpweven  12880  2sqpwodd  12881  dfphi2  12925  phimullem  12930  eulerthlemrprm  12934  phisum  12946  expnprm  13059  1arith  13073  4sqlem18  13114  ballotfilem4  13163  oddennn  13164  znnen  13170  ennnfonelemg  13175  ctinf  13202  mndid  13659  mhmf  13699  mhmlin  13701  mhm0  13702  grpinvex  13744  grplinv  13784  mulgz  13888  mulgdirlem  13891  mulgdir  13892  mulgass  13897  nsgbi  13942  nmzbi  13947  ghmf  13985  ghmlin  13986  conjnsg  14019  ablcmn  14029  cmncom  14040  crngmgp  14169  rhmmhm  14326  rhmghm  14329  rimf1o  14337  nzrnz  14349  subrgss  14390  subrg1cl  14397  rrgeq0i  14432  domneq0  14441  fldcrngd  14476  2idlelbas  14713  2idlcpblrng  14720  znidomb  14855  toponuni  14929  tpsuni  14948  neipsm  15068  cnf  15118  cnima  15134  txdis1cn  15192  hmeocnvcn  15220  psmetxrge0  15246  isxmet2d  15262  xmstopn  15369  mstopn  15370  bdxmet  15415  divcnap  15479  ivthinclemlr  15551  ivthinclemur  15553  dvlemap  15594  dvcnp2cntop  15613  dvaddxxbr  15615  dvmulxxbr  15616  dvcoapbr  15621  dvcjbr  15622  dvrecap  15627  dveflem  15640  plyf  15651  plyadd  15665  plymul  15666  plycn  15676  dvply2g  15680  dvdsppwf1o  15906  mpodvdsmulf1o  15907  lgsfle1  15931  lgsle1  15937  lgsdirprm  15956  lgsne0  15960  lgsquadlem1  15999  lgsquadlem2  16000  upgr1or2  16145  umgredg2en  16153  lfgredg2dom  16176  upgr2wlkdc  16421  trlres  16434  clwwlknon  16473  bj-indsuc  16747  nnsf  16832