Theorem simplbi 268

Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)

Hypothesis

Ref	Expression
simplbi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simplbi	⊢ (𝜑 → 𝜓)

Proof of Theorem simplbi

Step	Hyp	Ref	Expression
1		simplbi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	biimpi 118	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simpld 110	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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm5.62dc  886  3simpa  935  xoror  1310  anxordi  1331  sbidm  1772  reurex  2567  eqimss  3051  eldifi  3094  inss1  3186  sopo  4068  wefr  4113  ordtr  4133  opelxp1  4395  relop  4504  funmo  4937  funrel  4939  fnfun  5016  ffn  5066  f1f  5112  f1of1  5145  f1ofo  5153  isof1o  5467  eqopi  5818  1st2nd2  5821  reldmtpos  5891  swoer  6157  ecopover  6227  ecopoverg  6230  fnfi  6388  dfplpq2  6544  enq0ref  6623  cauappcvgprlemopl  6836  cauappcvgprlemdisj  6841  caucvgprlemopl  6859  caucvgprlemdisj  6864  caucvgprprlemopl  6887  caucvgprprlemopu  6889  caucvgprprlemdisj  6892  peano1nnnn  7020  axrnegex  7045  ltxrlt  7178  1nn  8050  zre  8355  nnssz  8368  ixxss1  8927  ixxss2  8928  ixxss12  8929  iccss2  8967  rge0ssre  9000  elfzuz  9041  uzdisj  9110  nn0disj  9148  frecuzrdgfn  9414  prmnn  10492  prmuz2  10512  oddpwdc  10552  sqpweven  10553  2sqpwodd  10554  bj-indint  10726  bj-inf2vnlem2  10766