Metamath Proof Explorer

Theorem simplbda

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

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

Proof

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