Theorem syl1111anc 837

Description: Four-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc 1373 except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017.)

Hypotheses

Ref	Expression
syl1111anc.1	⊢ (𝜑 → 𝜓)
syl1111anc.2	⊢ (𝜑 → 𝜒)
syl1111anc.3	⊢ (𝜑 → 𝜃)
syl1111anc.4	⊢ (𝜑 → 𝜏)
syl1111anc.5	⊢ ((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)

Assertion

Ref	Expression
syl1111anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl1111anc

Step	Hyp	Ref	Expression
1		syl1111anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl1111anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 511	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl1111anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl1111anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl1111anc.5	. 2 ⊢ ((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	3, 4, 5, 6	syl21anc 835	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396

This theorem is referenced by:  mpsyl4anc  839  ucnima  24007  f1otrge  28387  swrdf1  32384  mgcf1o  32437  cycpmrn  32569  linds2eq  32768  rhmimaidl  32821  idlmulssprm  32831  isprmidlc  32837  prmidlc  32838  qsidomlem2  32843  lbsdiflsp0  32996  extdg1id  33027  3cubeslem1  41725  cantnftermord  42373  sineq0ALT  44001  cncfshift  44890  cncfperiod  44895