Theorem simplbi 446

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

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  3simpa  952  reurex  2825  eqimss  3323  pssss  3364  eldifi  3388  inss1  3475  ssunsn2  3865  fnfun  5181  ffn  5223  f1f  5258  f1of1  5286  f1ofo  5293  nfvres  5352  ressnop0  5436  isof1o  5488  1stfo  5505  oprabid  5550  brtxp  5783  otelins2  5791  otelins3  5792  oqelins4  5794  weds  5938  ersym  5952  nchoicelem4  6292  nchoicelem8  6296  nchoicelem9  6297  nchoicelem19  6307  fnfreclem3  6319