Theorem H15NH16TH15IH16 41164

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

Hypotheses

Ref	Expression
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

Ref	Expression
H15NH16TH15IH16	|- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) /\ ka ) /\ jph ) /\ jps ) /\ jch ) -> jth )

Proof of Theorem H15NH16TH15IH16

Step	Hyp	Ref	Expression
1		H15NH16TH15IH16.16	. 2 |- jth
2	1	a1i 11	1 |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) /\ ka ) /\ jph ) /\ jps ) /\ jch ) -> jth )

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6

This theorem is referenced by: (None)