Theorem H15NH16TH15IH16 46943

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	⊢ 𝜑
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

Ref	Expression
H15NH16TH15IH16	⊢ (((((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ jph) ∧ jps) ∧ jch) → jth)

Proof of Theorem H15NH16TH15IH16

Step	Hyp	Ref	Expression
1		H15NH16TH15IH16.16	. 2 ⊢ jth
2	1	a1i 11	1 ⊢ (((((((((((((((𝜑 ∧ 𝜓) ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) ∧ 𝜌) ∧ 𝜇) ∧ 𝜆) ∧ 𝜅) ∧ jph) ∧ jps) ∧ jch) → jth)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by: (None)