Theorem syl211anc 1356

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

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

Assertion

Ref	Expression
syl211anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl211anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 504	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl211anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂)
7	3, 4, 5, 6	syl3anc 1351	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  syl212anc  1360  syl221anc  1361  supicc  12702  modaddmulmod  13121  limsupgre  14699  limsupbnd1  14700  limsupbnd2  14701  lbspss  19576  lindff1  20666  islinds4  20681  mdetunilem9  20933  madutpos  20955  neiptopnei  21444  mbflimsup  23970  cxpneg  24965  cxpmul2  24973  cxpsqrt  24987  cxpaddd  25001  cxpsubd  25002  divcxpd  25006  fsumharmonic  25291  bposlem1  25562  lgsqr  25629  chpchtlim  25757  ax5seg  26427  archiabllem2c  30487  logdivsqrle  31566  frrlem15  32660  lindsadd  34323  lshpnelb  35562  cdlemg2fv2  37178  cdlemg2m  37182  cdlemg9a  37210  cdlemg9b  37211  cdlemg12b  37222  cdlemg14f  37231  cdlemg14g  37232  cdlemg17dN  37241  cdlemkj  37441  cdlemkuv2  37445  cdlemk52  37532  cdlemk53a  37533  mullimc  41326  mullimcf  41333  sfprmdvdsmersenne  43134  lincfsuppcl  43833