Theorem H15NH16TH15IH16

Description: Given 15 hypotheses and a 16th hypothesis, there exists a proof the 15 imply the 16th. (Contributed by Jarvin Udandy, 8-Sep-2016)

	Ref	Expression
Hypotheses	H15NH16TH15IH16.1	⊢ 𝜑
	H15NH16TH15IH16.2	⊢ 𝜓
	H15NH16TH15IH16.3	⊢ 𝜒
	H15NH16TH15IH16.4	⊢ 𝜃
	H15NH16TH15IH16.5	⊢ 𝜏
	H15NH16TH15IH16.6	⊢ 𝜂
	H15NH16TH15IH16.7	⊢ 𝜁
	H15NH16TH15IH16.8	⊢ 𝜎
	H15NH16TH15IH16.9	⊢ 𝜌
	H15NH16TH15IH16.10	⊢ 𝜇
	H15NH16TH15IH16.11	⊢ 𝜆
	H15NH16TH15IH16.12	⊢ 𝜅
	H15NH16TH15IH16.13	⊢ jph
	H15NH16TH15IH16.14	⊢ jps
	H15NH16TH15IH16.15	⊢ jch
	H15NH16TH15IH16.16	⊢ jth
Assertion	H15NH16TH15IH16	⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) ∧ 𝜁 ) ∧ 𝜎 ) ∧ 𝜌 ) ∧ 𝜇 ) ∧ 𝜆 ) ∧ 𝜅 ) ∧ jph ) ∧ jps ) ∧ jch ) → jth )

Proof

Step	Hyp	Ref	Expression
1		H15NH16TH15IH16.1	⊢ 𝜑
2		H15NH16TH15IH16.2	⊢ 𝜓
3		H15NH16TH15IH16.3	⊢ 𝜒
4		H15NH16TH15IH16.4	⊢ 𝜃
5		H15NH16TH15IH16.5	⊢ 𝜏
6		H15NH16TH15IH16.6	⊢ 𝜂
7		H15NH16TH15IH16.7	⊢ 𝜁
8		H15NH16TH15IH16.8	⊢ 𝜎
9		H15NH16TH15IH16.9	⊢ 𝜌
10		H15NH16TH15IH16.10	⊢ 𝜇
11		H15NH16TH15IH16.11	⊢ 𝜆
12		H15NH16TH15IH16.12	⊢ 𝜅
13		H15NH16TH15IH16.13	⊢ jph
14		H15NH16TH15IH16.14	⊢ jps
15		H15NH16TH15IH16.15	⊢ jch
16		H15NH16TH15IH16.16	⊢ jth
17	16	a1i	⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) ∧ 𝜂 ) ∧ 𝜁 ) ∧ 𝜎 ) ∧ 𝜌 ) ∧ 𝜇 ) ∧ 𝜆 ) ∧ 𝜅 ) ∧ jph ) ∧ jps ) ∧ jch ) → jth )