Metamath Proof Explorer

Theorem simplbi

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

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

Proof

Step Hyp Ref Expression
1 simplbi.1 
 |-  ( ph <-> ( ps /\ ch ) )
2 1 biimpi 
 |-  ( ph -> ( ps /\ ch ) )
3 2 simpld 
 |-  ( ph -> ps )