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  18519  ucnima  24188  f1otrge  28843  swrdf1  32927  mgcf1o  32974  gsumfs2d  33025  cycpmrn  33102  linds2eq  33336  rhmimaidl  33387  idlmulssprm  33397  isprmidlc  33402  prmidlc  33403  qsidomlem2  33408  ply1unit  33528  lbsdiflsp0  33629  extdg1id  33669  3cubeslem1  42696  cantnftermord  43332  sineq0ALT  44948  cncfshift  45891  cncfperiod  45896