Theorem syl1111anc 840

Description: Four-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc 1376 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 837	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 207  df-an 396

This theorem is referenced by:  mpsyl4anc  842  chnind  18529  ucnima  24196  f1otrge  28851  swrdf1  32944  mgcf1o  32991  gsumfs2d  33042  cycpmrn  33119  linds2eq  33353  rhmimaidl  33404  idlmulssprm  33414  isprmidlc  33419  prmidlc  33420  qsidomlem2  33425  ply1unit  33545  lbsdiflsp0  33660  extdg1id  33700  3cubeslem1  42802  cantnftermord  43438  sineq0ALT  45054  cncfshift  45997  cncfperiod  46002