Theorem simplbi 259

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 113	. 2 ⊢ (φ → (ψ ∧ χ))
3	2	simpld 105	1 ⊢ (φ → ψ)

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm5.62dc  840  3simpa  889  anxordi  1274  sbidm  1713  reurex  2501  eqimss  2974  pssss  3016  eldifi  3043  inss1  3134  sopo  4024  ordtr  4064  opelxp1  4304  relop  4413  funmo  4843  funrel  4845  fnfun  4922  ffn  4972  f1f  5017  f1of1  5050  f1ofo  5058  isof1o  5372  eqopi  5721  1st2nd2  5724  reldmtpos  5790  swoer  6045  ecopover  6115  ecopoverg  6118  dfplpq2  6213  enq0ref  6288  axrnegex  6573  ltxrlt  6686  bj-indint  7301  bj-inf2vnlem2  7336