Theorem simplbi2

Description: Deduction eliminating a conjunct. (Contributed by Alan Sare, 31-Dec-2011)

	Ref	Expression
Hypothesis	simplbi2.1	⊢ ( 𝜑 ↔ ( 𝜓 ∧ 𝜒 ) )
Assertion	simplbi2	⊢ ( 𝜓 → ( 𝜒 → 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		simplbi2.1	⊢ ( 𝜑 ↔ ( 𝜓 ∧ 𝜒 ) )
2	1	biimpri	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜑 )
3	2	ex	⊢ ( 𝜓 → ( 𝜒 → 𝜑 ) )