Theorem ad5ant135OLD

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

Proof

ad5ant.1

ad4ant134 _

adantlr _