Metamath Proof Explorer

Theorem simprbda

Description: Deduction eliminating a conjunct. (Contributed by NM, 22-Oct-2007)

Ref Expression
Hypothesis pm3.26bda.1 
|- ( ph -> ( ps <-> ( ch /\ th ) ) )
Assertion simprbda 
|- ( ( ph /\ ps ) -> ch )

Proof

Step Hyp Ref Expression
1 pm3.26bda.1 
 |-  ( ph -> ( ps <-> ( ch /\ th ) ) )
2 1 biimpa 
 |-  ( ( ph /\ ps ) -> ( ch /\ th ) )
3 2 simpld 
 |-  ( ( ph /\ ps ) -> ch )