Metamath Proof Explorer

Theorem simprbi

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

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

Proof

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