Theorem syl1111anc 854

Description: Four-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc 1402 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 521	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl1111anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl1111anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl1111anc.5	. 2 ⊢ ((((𝜓 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)
7	3, 4, 5, 6	syl21anc 851	1 ⊢ (𝜑 → 𝜂)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  mpsyl4anc  856  swrdf1  14841  chnind  18845  idlmulssprm  21674  isprmidlc  21679  prmidlc  21680  qsidomlem2  21688  ucnima  24654  f1otrge  29506  mgcf1o  33663  gsumfs2d  33721  cycpmrn  33803  rlocisunit  33936  linds2eq  34040  rhmimaidl  34086  ply1unit  34210  lbsdiflsp0  34369  extdg1id  34409  3cubeslem1  43960  cantnftermord  44583  sineq0ALT  46179  cncfshift  47157  cncfperiod  47162  line2x  50197  inlinecirc02plem  50229