Theorem ad11antr

Description: Deduction adding 11 conjuncts to antecedent. (Contributed by Thierry Arnoux, 27-Sep-2025) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ad11antr.1	⊢ ( 𝜑 → 𝜓 )
Assertion	ad11antr	⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) ∧ 𝜁 ) ∧ 𝜎 ) ∧ 𝜌 ) ∧ 𝜇 ) ∧ 𝜆 ) ∧ 𝜅 ) ∧ 𝜈 ) → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		ad11antr.1	⊢ ( 𝜑 → 𝜓 )
2	1	adantr	⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝜓 )
3	2	ad10antr	⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) ∧ 𝜁 ) ∧ 𝜎 ) ∧ 𝜌 ) ∧ 𝜇 ) ∧ 𝜆 ) ∧ 𝜅 ) ∧ 𝜈 ) → 𝜓 )