Theorem syl1111anc 839

Description: Four-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc 1374 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  841  ucnima  24311  f1otrge  28898  swrdf1  32923  mgcf1o  32976  chnind  32983  cycpmrn  33136  linds2eq  33374  rhmimaidl  33425  idlmulssprm  33435  isprmidlc  33440  prmidlc  33441  qsidomlem2  33446  ply1unit  33565  lbsdiflsp0  33639  extdg1id  33676  3cubeslem1  42640  cantnftermord  43282  sineq0ALT  44908  cncfshift  45795  cncfperiod  45800