Theorem ad5ant134OLD

Obsolete version of ad5ant134 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 \tau \wedge \psi \wedge \chi \wedge \eta \rightarrow \theta \)

Proof

ad5ant.1

ad4ant134 _

adantr _