Theorem simprbi 270

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 119	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 113	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm5.63dc  893  sb1  1697  reurmo  2582  eldifn  3124  elinel2  3188  rabsnt  3521  eldifsni  3575  unimax  3693  ssintub  3712  moop2  4087  wepo  4195  wetrep  4196  trssord  4216  ordelord  4217  ordsucim  4330  ordtri2or2exmidlem  4355  regexmidlem1  4362  reg2exmidlema  4363  tfis  4411  opelxp2  4486  funmo  5043  funopg  5061  funco  5067  funun  5071  fununi  5095  funimaexglem  5110  fndm  5126  frn  5182  f1ss  5235  f1ssr  5236  f1ssres  5238  forn  5249  f1f1orn  5277  f1orescnv  5282  f1imacnv  5283  funcocnv2  5291  funfveu  5331  nfvres  5350  foelrnOLD  5546  isorel  5601  isoini2  5612  f1ofveu  5654  fovcl  5764  f1opw  5865  f1o2ndf1  6007  mpt2xopn0yelv  6018  swoer  6334  mapsnconst  6465  en0  6566  en1  6570  phplem4  6625  phplem4dom  6632  phplem4on  6637  ssfilem  6645  diffitest  6657  inffiexmid  6676  supubti  6748  suplubti  6749  djuinr  6809  casefun  6830  casef1  6835  djufun  6840  exmidfodomrlemim  6888  0npi  6933  mulclpi  6948  mulcanpig  6955  nlt1pig  6961  indpi  6962  nnppipi  6963  dfplpq2  6974  archnqq  7037  enq0tr  7054  nqnq0pi  7058  ltexprlemopl  7221  ltexprlemopu  7223  cauappcvgprlemopl  7266  cauappcvgprlemlol  7267  cauappcvgprlemopu  7268  cauappcvgprlemupu  7269  cauappcvgprlemdisj  7271  caucvgprlemopl  7289  caucvgprlemlol  7290  caucvgprlemopu  7291  caucvgprlemupu  7292  caucvgprlemdisj  7294  caucvgprprlemopl  7317  caucvgprprlemlol  7318  caucvgprprlemopu  7319  caucvgprprlemupu  7320  caucvgprprlemdisj  7322  ltresr2  7438  peano2nnnn  7451  axrnegex  7475  ltxrlt  7613  peano2nn  8495  elnn0z  8824  zaddcl  8851  ztri3or0  8853  eluz2gt1  9150  1nuz2  9154  rpgt0  9206  ixxss1  9383  ixxss2  9384  ixxss12  9385  iccss2  9423  iccssico2  9426  elfzuz3  9498  uzdisj  9568  nn0disj  9610  addmodlteq  9866  expge0  10052  expge1  10053  expaddzaplem  10059  shftfn  10319  fsumf1o  10843  fsumge0  10914  zsupcllemstep  11280  bezoutlemzz  11330  bezoutlemaz  11331  bezoutlembz  11332  bezoutlemsup  11337  1nprm  11435  nprm  11444  sqnprm  11456  dvdsprm  11457  coprm  11462  sqpweven  11492  2sqpwodd  11493  dfphi2  11535  phimullem  11540  oddennn  11544  znnen  11550  toponuni  11775  tpsuni  11793  bj-indsuc  12096  nnsf  12167  nninfalllemn  12170