Metamath Proof Explorer


Theorem 2a1d

Description: Deduction introducing two antecedents. Two applications of a1d . Deduction associated with 2a1 and 2a1i . (Contributed by BJ, 10-Aug-2020)

Ref Expression
Hypothesis 2a1d.1 φψ
Assertion 2a1d φχθψ

Proof

Step Hyp Ref Expression
1 2a1d.1 φψ
2 1 a1d φθψ
3 2 a1d φχθψ