Metamath Proof Explorer


Theorem simplbda

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

Ref Expression
Hypothesis pm3.26bda.1 φψχθ
Assertion simplbda φψθ

Proof

Step Hyp Ref Expression
1 pm3.26bda.1 φψχθ
2 1 biimpa φψχθ
3 2 simprd φψθ