Metamath Proof Explorer


Theorem a2d

Description: Deduction distributing an embedded antecedent. Deduction form of ax-2 . (Contributed by NM, 23-Jun-1994)

Ref Expression
Hypothesis a2d.1 φψχθ
Assertion a2d φψχψθ

Proof

Step Hyp Ref Expression
1 a2d.1 φψχθ
2 ax-2 ψχθψχψθ
3 1 2 syl φψχψθ