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	|- ph
	H15NH16TH15IH16.2	|- ps
	H15NH16TH15IH16.3	|- ch
	H15NH16TH15IH16.4	|- th
	H15NH16TH15IH16.5	|- ta
	H15NH16TH15IH16.6	|- et
	H15NH16TH15IH16.7	|- ze
	H15NH16TH15IH16.8	|- si
	H15NH16TH15IH16.9	|- rh
	H15NH16TH15IH16.10	|- mu
	H15NH16TH15IH16.11	|- la
	H15NH16TH15IH16.12	|- ka
	H15NH16TH15IH16.13	|- jph
	H15NH16TH15IH16.14	|- jps
	H15NH16TH15IH16.15	|- jch
	H15NH16TH15IH16.16	|- jth
Assertion	H15NH16TH15IH16	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) /\ ka ) /\ jph ) /\ jps ) /\ jch ) -> jth )

Proof

Step	Hyp	Ref	Expression
1		H15NH16TH15IH16.1	|- ph
2		H15NH16TH15IH16.2	|- ps
3		H15NH16TH15IH16.3	|- ch
4		H15NH16TH15IH16.4	|- th
5		H15NH16TH15IH16.5	|- ta
6		H15NH16TH15IH16.6	|- et
7		H15NH16TH15IH16.7	|- ze
8		H15NH16TH15IH16.8	|- si
9		H15NH16TH15IH16.9	|- rh
10		H15NH16TH15IH16.10	|- mu
11		H15NH16TH15IH16.11	|- la
12		H15NH16TH15IH16.12	|- ka
13		H15NH16TH15IH16.13	|- jph
14		H15NH16TH15IH16.14	|- jps
15		H15NH16TH15IH16.15	|- jch
16		H15NH16TH15IH16.16	|- jth
17	16	a1i	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) /\ ka ) /\ jph ) /\ jps ) /\ jch ) -> jth )