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  948  sb1  1777  reurmo  2705  eldifn  3273  elinel2  3337  rabsnt  3682  eldifsni  3736  unimax  3858  ssintub  3877  exmidsssnc  4218  moop2  4266  wepo  4374  wetrep  4375  trssord  4395  ordelord  4396  ordsucim  4514  ordtri2or2exmidlem  4540  regexmidlem1  4547  reg2exmidlema  4548  tfis  4597  opelxp2  4676  funmo  5246  funopg  5265  funco  5271  funun  5275  fununi  5299  funimaexglem  5314  fndm  5330  frn  5389  f1ss  5442  f1ssr  5443  f1ssres  5445  forn  5456  f1f1orn  5487  f1orescnv  5492  f1imacnv  5493  funcocnv2  5501  funfveu  5543  nfvres  5563  isorel  5825  isoini2  5836  f1ofveu  5879  fovcld  5996  f1opw  6096  f1o2ndf1  6247  mpoxopn0yelv  6258  swoer  6581  mapsnconst  6712  en0  6813  en1  6817  phplem4  6873  phplem4dom  6880  phplem4on  6885  ssfilem  6893  diffitest  6905  inffiexmid  6924  supubti  7016  suplubti  7017  djuinr  7080  casefun  7102  casef1  7107  djufun  7121  nnnninfeq  7144  ctssexmid  7166  exmidonfinlem  7210  exmidfodomrlemim  7218  cc4f  7286  cc4n  7288  0npi  7330  mulclpi  7345  mulcanpig  7352  nlt1pig  7358  indpi  7359  nnppipi  7360  dfplpq2  7371  archnqq  7434  enq0tr  7451  nqnq0pi  7455  ltexprlemopl  7618  ltexprlemopu  7620  cauappcvgprlemopl  7663  cauappcvgprlemlol  7664  cauappcvgprlemopu  7665  cauappcvgprlemupu  7666  cauappcvgprlemdisj  7668  caucvgprlemopl  7686  caucvgprlemlol  7687  caucvgprlemopu  7688  caucvgprlemupu  7689  caucvgprlemdisj  7691  caucvgprprlemopl  7714  caucvgprprlemlol  7715  caucvgprprlemopu  7716  caucvgprprlemupu  7717  caucvgprprlemdisj  7719  suplocsrlempr  7824  ltresr2  7857  peano2nnnn  7870  axrnegex  7896  ltxrlt  8041  peano2nn  8949  elnn0z  9284  zaddcl  9311  ztri3or0  9313  eluz2gt1  9620  1nuz2  9624  rpgt0  9683  ixxss1  9922  ixxss2  9923  ixxss12  9924  iccss2  9962  iccssico2  9965  elfzuz3  10040  uzdisj  10111  nn0disj  10156  addmodlteq  10416  expge0  10574  expge1  10575  expaddzaplem  10581  shftfn  10851  fsumf1o  11416  fsumge0  11485  fprodf1o  11614  zsupcllemstep  11964  zsupssdc  11973  bezoutlemzz  12021  bezoutlemaz  12022  bezoutlembz  12023  bezoutlemsup  12028  1nprm  12132  nprm  12141  sqnprm  12154  dvdsprm  12155  coprm  12162  sqpweven  12193  2sqpwodd  12194  dfphi2  12238  phimullem  12243  eulerthlemrprm  12247  phisum  12258  expnprm  12369  1arith  12383  oddennn  12411  znnen  12417  ennnfonelemg  12422  ctinf  12449  mndid  12852  mhmf  12883  mhmlin  12885  mhm0  12886  grpinvex  12921  grplinv  12960  mulgz  13056  mulgdirlem  13059  mulgdir  13060  mulgass  13065  nsgbi  13109  nmzbi  13114  ghmf  13147  ghmlin  13148  conjnsg  13181  ablcmn  13191  cmncom  13202  crngmgp  13319  rhmmhm  13470  rhmghm  13473  rimf1o  13481  nzrnz  13493  subrgss  13530  subrg1cl  13537  2idlelbas  13792  2idlcpblrng  13799  toponuni  13912  tpsuni  13931  neipsm  14051  cnf  14101  cnima  14117  txdis1cn  14175  hmeocnvcn  14203  psmetxrge0  14229  isxmet2d  14245  xmstopn  14352  mstopn  14353  bdxmet  14398  divcnap  14452  ivthinclemlr  14512  ivthinclemur  14514  dvlemap  14546  dvcnp2cntop  14560  dvaddxxbr  14562  dvmulxxbr  14563  dvcoapbr  14568  dvcjbr  14569  dvrecap  14574  dveflem  14584  lgsfle1  14807  lgsle1  14813  lgsdirprm  14832  lgsne0  14836  bj-indsuc  15077  nnsf  15152