Theorem ad5ant124OLD

Obsolete version of ad5ant124 as of 13-Jun-2026. Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 23-Jun-2022.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis
ad5ant.1
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \psi \wedge \tau \wedge \chi \wedge \eta \rightarrow \theta \)
Proof
ad5ant.1
ad4ant124 _
adantr _