Metamath Proof Explorer

Theorem simplbi2

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

Ref Expression
Hypothesis simplbi2.1 
|- ( ph <-> ( ps /\ ch ) )
Assertion simplbi2 
|- ( ps -> ( ch -> ph ) )

Proof

Step Hyp Ref Expression
1 simplbi2.1 
 |-  ( ph <-> ( ps /\ ch ) )
2 1 biimpri 
 |-  ( ( ps /\ ch ) -> ph )
3 2 ex 
 |-  ( ps -> ( ch -> ph ) )