Metamath Proof Explorer


Theorem 3adant2

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995)

Ref Expression
Hypothesis 3adant.1 φ ψ χ
Assertion 3adant2 φ θ ψ χ

Proof

Step Hyp Ref Expression
1 3adant.1 φ ψ χ
2 1 adantlr φ θ ψ χ
3 2 3impa φ θ ψ χ