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