Metamath Proof Explorer


Theorem 3adant3r2

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 17-Feb-2008)

Ref Expression
Hypothesis ad4ant3.1 φ ψ χ θ
Assertion 3adant3r2 φ ψ τ χ θ

Proof

Step Hyp Ref Expression
1 ad4ant3.1 φ ψ χ θ
2 1 3expb φ ψ χ θ
3 2 3adantr2 φ ψ τ χ θ