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  2691  eldifn  3258  elinel2  3322  rabsnt  3667  eldifsni  3721  unimax  3843  ssintub  3862  exmidsssnc  4203  moop2  4251  wepo  4359  wetrep  4360  trssord  4380  ordelord  4381  ordsucim  4499  ordtri2or2exmidlem  4525  regexmidlem1  4532  reg2exmidlema  4533  tfis  4582  opelxp2  4661  funmo  5231  funopg  5250  funco  5256  funun  5260  fununi  5284  funimaexglem  5299  fndm  5315  frn  5374  f1ss  5427  f1ssr  5428  f1ssres  5430  forn  5441  f1f1orn  5472  f1orescnv  5477  f1imacnv  5478  funcocnv2  5486  funfveu  5528  nfvres  5548  isorel  5808  isoini2  5819  f1ofveu  5862  fovcl  5979  f1opw  6077  f1o2ndf1  6228  mpoxopn0yelv  6239  swoer  6562  mapsnconst  6693  en0  6794  en1  6798  phplem4  6854  phplem4dom  6861  phplem4on  6866  ssfilem  6874  diffitest  6886  inffiexmid  6905  supubti  6997  suplubti  6998  djuinr  7061  casefun  7083  casef1  7088  djufun  7102  nnnninfeq  7125  ctssexmid  7147  exmidonfinlem  7191  exmidfodomrlemim  7199  cc4f  7267  cc4n  7269  0npi  7311  mulclpi  7326  mulcanpig  7333  nlt1pig  7339  indpi  7340  nnppipi  7341  dfplpq2  7352  archnqq  7415  enq0tr  7432  nqnq0pi  7436  ltexprlemopl  7599  ltexprlemopu  7601  cauappcvgprlemopl  7644  cauappcvgprlemlol  7645  cauappcvgprlemopu  7646  cauappcvgprlemupu  7647  cauappcvgprlemdisj  7649  caucvgprlemopl  7667  caucvgprlemlol  7668  caucvgprlemopu  7669  caucvgprlemupu  7670  caucvgprlemdisj  7672  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemopu  7697  caucvgprprlemupu  7698  caucvgprprlemdisj  7700  suplocsrlempr  7805  ltresr2  7838  peano2nnnn  7851  axrnegex  7877  ltxrlt  8022  peano2nn  8930  elnn0z  9265  zaddcl  9292  ztri3or0  9294  eluz2gt1  9601  1nuz2  9605  rpgt0  9664  ixxss1  9903  ixxss2  9904  ixxss12  9905  iccss2  9943  iccssico2  9946  elfzuz3  10021  uzdisj  10092  nn0disj  10137  addmodlteq  10397  expge0  10555  expge1  10556  expaddzaplem  10562  shftfn  10832  fsumf1o  11397  fsumge0  11466  fprodf1o  11595  zsupcllemstep  11945  zsupssdc  11954  bezoutlemzz  12002  bezoutlemaz  12003  bezoutlembz  12004  bezoutlemsup  12009  1nprm  12113  nprm  12122  sqnprm  12135  dvdsprm  12136  coprm  12143  sqpweven  12174  2sqpwodd  12175  dfphi2  12219  phimullem  12224  eulerthlemrprm  12228  phisum  12239  expnprm  12350  1arith  12364  oddennn  12392  znnen  12398  ennnfonelemg  12403  ctinf  12430  mndid  12825  mhmf  12855  mhmlin  12857  mhm0  12858  grpinvex  12886  grplinv  12921  mulgz  13009  mulgdirlem  13012  mulgdir  13013  mulgass  13018  nsgbi  13062  nmzbi  13067  ablcmn  13093  cmncom  13103  crngmgp  13185  nzrnz  13324  subrgss  13341  subrg1cl  13348  toponuni  13485  tpsuni  13504  neipsm  13624  cnf  13674  cnima  13690  txdis1cn  13748  hmeocnvcn  13776  psmetxrge0  13802  isxmet2d  13818  xmstopn  13925  mstopn  13926  bdxmet  13971  divcnap  14025  ivthinclemlr  14085  ivthinclemur  14087  dvlemap  14119  dvcnp2cntop  14133  dvaddxxbr  14135  dvmulxxbr  14136  dvcoapbr  14141  dvcjbr  14142  dvrecap  14147  dveflem  14157  lgsfle1  14380  lgsle1  14386  lgsdirprm  14405  lgsne0  14409  bj-indsuc  14650  nnsf  14724