Theorem simprbi 269

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm5.63dc  887  sb1  1689  reurmo  2568  eldifn  3095  rabsnt  3467  eldifsni  3518  unimax  3635  ssintub  3654  moop2  4006  wepo  4114  wetrep  4115  trssord  4135  ordelord  4136  ordsucim  4244  ordtri2or2exmidlem  4269  regexmidlem1  4276  reg2exmidlema  4277  tfis  4324  opelxp2  4396  funmo  4937  funopg  4954  funco  4960  funun  4964  fununi  4987  funimaexglem  5002  fndm  5018  frn  5072  f1ss  5117  f1ssr  5118  f1ssres  5119  forn  5129  f1f1orn  5157  f1orescnv  5162  f1imacnv  5163  funcocnv2  5171  funfveu  5208  nfvres  5227  foelrn  5338  isorel  5468  isoini2  5478  f1ofveu  5520  fovcl  5626  f1opw  5727  f1o2ndf1  5869  mpt2xopn0yelv  5877  swoer  6157  en0  6298  en1  6302  phplem4  6341  phplem4dom  6348  phplem4on  6353  ssfilem  6360  diffitest  6371  supubti  6412  suplubti  6413  0npi  6503  mulclpi  6518  mulcanpig  6525  nlt1pig  6531  indpi  6532  nnppipi  6533  dfplpq2  6544  archnqq  6607  enq0tr  6624  nqnq0pi  6628  ltexprlemopl  6791  ltexprlemopu  6793  cauappcvgprlemopl  6836  cauappcvgprlemlol  6837  cauappcvgprlemopu  6838  cauappcvgprlemupu  6839  cauappcvgprlemdisj  6841  caucvgprlemopl  6859  caucvgprlemlol  6860  caucvgprlemopu  6861  caucvgprlemupu  6862  caucvgprlemdisj  6864  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemopu  6889  caucvgprprlemupu  6890  caucvgprprlemdisj  6892  ltresr2  7008  peano2nnnn  7021  axrnegex  7045  ltxrlt  7178  peano2nn  8051  elnn0z  8364  zaddcl  8391  ztri3or0  8393  eluz2gt1  8689  1nuz2  8693  rpgt0  8745  ixxss1  8927  ixxss2  8928  ixxss12  8929  iccss2  8967  iccssico2  8970  elfzuz3  9042  uzdisj  9110  nn0disj  9148  addmodlteq  9400  serige0  9473  expge0  9512  expge1  9513  expaddzaplem  9519  shftfn  9712  zsupcllemstep  10341  bezoutlemzz  10391  bezoutlemaz  10392  bezoutlembz  10393  bezoutlemsup  10398  1nprm  10496  nprm  10505  sqnprm  10517  dvdsprm  10518  coprm  10523  sqpweven  10553  2sqpwodd  10554  bj-indsuc  10723