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 φ χ θ ψ