Theorem ad5ant125OLD

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

Proof

ad5ant.1

3expia _

2a1d _

imp41 _