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  946  sb1  1766  reurmo  2692  eldifn  3260  elinel2  3324  rabsnt  3669  eldifsni  3723  unimax  3845  ssintub  3864  exmidsssnc  4205  moop2  4253  wepo  4361  wetrep  4362  trssord  4382  ordelord  4383  ordsucim  4501  ordtri2or2exmidlem  4527  regexmidlem1  4534  reg2exmidlema  4535  tfis  4584  opelxp2  4663  funmo  5233  funopg  5252  funco  5258  funun  5262  fununi  5286  funimaexglem  5301  fndm  5317  frn  5376  f1ss  5429  f1ssr  5430  f1ssres  5432  forn  5443  f1f1orn  5474  f1orescnv  5479  f1imacnv  5480  funcocnv2  5488  funfveu  5530  nfvres  5550  isorel  5811  isoini2  5822  f1ofveu  5865  fovcl  5982  f1opw  6080  f1o2ndf1  6231  mpoxopn0yelv  6242  swoer  6565  mapsnconst  6696  en0  6797  en1  6801  phplem4  6857  phplem4dom  6864  phplem4on  6869  ssfilem  6877  diffitest  6889  inffiexmid  6908  supubti  7000  suplubti  7001  djuinr  7064  casefun  7086  casef1  7091  djufun  7105  nnnninfeq  7128  ctssexmid  7150  exmidonfinlem  7194  exmidfodomrlemim  7202  cc4f  7270  cc4n  7272  0npi  7314  mulclpi  7329  mulcanpig  7336  nlt1pig  7342  indpi  7343  nnppipi  7344  dfplpq2  7355  archnqq  7418  enq0tr  7435  nqnq0pi  7439  ltexprlemopl  7602  ltexprlemopu  7604  cauappcvgprlemopl  7647  cauappcvgprlemlol  7648  cauappcvgprlemopu  7649  cauappcvgprlemupu  7650  cauappcvgprlemdisj  7652  caucvgprlemopl  7670  caucvgprlemlol  7671  caucvgprlemopu  7672  caucvgprlemupu  7673  caucvgprlemdisj  7675  caucvgprprlemopl  7698  caucvgprprlemlol  7699  caucvgprprlemopu  7700  caucvgprprlemupu  7701  caucvgprprlemdisj  7703  suplocsrlempr  7808  ltresr2  7841  peano2nnnn  7854  axrnegex  7880  ltxrlt  8025  peano2nn  8933  elnn0z  9268  zaddcl  9295  ztri3or0  9297  eluz2gt1  9604  1nuz2  9608  rpgt0  9667  ixxss1  9906  ixxss2  9907  ixxss12  9908  iccss2  9946  iccssico2  9949  elfzuz3  10024  uzdisj  10095  nn0disj  10140  addmodlteq  10400  expge0  10558  expge1  10559  expaddzaplem  10565  shftfn  10835  fsumf1o  11400  fsumge0  11469  fprodf1o  11598  zsupcllemstep  11948  zsupssdc  11957  bezoutlemzz  12005  bezoutlemaz  12006  bezoutlembz  12007  bezoutlemsup  12012  1nprm  12116  nprm  12125  sqnprm  12138  dvdsprm  12139  coprm  12146  sqpweven  12177  2sqpwodd  12178  dfphi2  12222  phimullem  12227  eulerthlemrprm  12231  phisum  12242  expnprm  12353  1arith  12367  oddennn  12395  znnen  12401  ennnfonelemg  12406  ctinf  12433  mndid  12831  mhmf  12861  mhmlin  12863  mhm0  12864  grpinvex  12892  grplinv  12927  mulgz  13016  mulgdirlem  13019  mulgdir  13020  mulgass  13025  nsgbi  13069  nmzbi  13074  ablcmn  13100  cmncom  13110  crngmgp  13192  nzrnz  13331  subrgss  13348  subrg1cl  13355  toponuni  13554  tpsuni  13573  neipsm  13693  cnf  13743  cnima  13759  txdis1cn  13817  hmeocnvcn  13845  psmetxrge0  13871  isxmet2d  13887  xmstopn  13994  mstopn  13995  bdxmet  14040  divcnap  14094  ivthinclemlr  14154  ivthinclemur  14156  dvlemap  14188  dvcnp2cntop  14202  dvaddxxbr  14204  dvmulxxbr  14205  dvcoapbr  14210  dvcjbr  14211  dvrecap  14216  dveflem  14226  lgsfle1  14449  lgsle1  14455  lgsdirprm  14474  lgsne0  14478  bj-indsuc  14719  nnsf  14793