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	$$⊢\phi$$
	H15NH16TH15IH16.2	$$⊢\psi$$
	H15NH16TH15IH16.3	$$⊢\chi$$
	H15NH16TH15IH16.4	$$⊢\theta$$
	H15NH16TH15IH16.5	$$⊢\tau$$
	H15NH16TH15IH16.6	$$⊢\eta$$
	H15NH16TH15IH16.7	$$⊢\zeta$$
	H15NH16TH15IH16.8	$$⊢\sigma$$
	H15NH16TH15IH16.9	$$⊢\rho$$
	H15NH16TH15IH16.10	$$⊢\mu$$
	H15NH16TH15IH16.11	$$⊢\lambda$$
	H15NH16TH15IH16.12	$$⊢\kappa$$
	H15NH16TH15IH16.13	No typesetting found for |- jph with typecode |-
	H15NH16TH15IH16.14	No typesetting found for |- jps with typecode |-
	H15NH16TH15IH16.15	No typesetting found for |- jch with typecode |-
	H15NH16TH15IH16.16	No typesetting found for |- jth with typecode |-
Assertion	H15NH16TH15IH16	Could not format assertion : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) /\ ka ) /\ jph ) /\ jps ) /\ jch ) -> jth ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		H15NH16TH15IH16.1	$$⊢\phi$$
2		H15NH16TH15IH16.2	$$⊢\psi$$
3		H15NH16TH15IH16.3	$$⊢\chi$$
4		H15NH16TH15IH16.4	$$⊢\theta$$
5		H15NH16TH15IH16.5	$$⊢\tau$$
6		H15NH16TH15IH16.6	$$⊢\eta$$
7		H15NH16TH15IH16.7	$$⊢\zeta$$
8		H15NH16TH15IH16.8	$$⊢\sigma$$
9		H15NH16TH15IH16.9	$$⊢\rho$$
10		H15NH16TH15IH16.10	$$⊢\mu$$
11		H15NH16TH15IH16.11	$$⊢\lambda$$
12		H15NH16TH15IH16.12	$$⊢\kappa$$
13		H15NH16TH15IH16.13	Could not format jph : No typesetting found for |- jph with typecode |-
14		H15NH16TH15IH16.14	Could not format jps : No typesetting found for |- jps with typecode |-
15		H15NH16TH15IH16.15	Could not format jch : No typesetting found for |- jch with typecode |-
16		H15NH16TH15IH16.16	Could not format jth : No typesetting found for |- jth with typecode |-
17	16	a1i	Could not format ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) /\ ka ) /\ jph ) /\ jps ) /\ jch ) -> jth ) : No typesetting found for |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) /\ ka ) /\ jph ) /\ jps ) /\ jch ) -> jth ) with typecode |-