Theorem syl211anc 1373

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 510	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl211anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂)
7	3, 4, 5, 6	syl3anc 1368	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  syl212anc  1377  syl221anc  1378  frrlem15  9807  supicc  13542  modaddmulmod  13969  limsupgre  15504  limsupbnd1  15505  limsupbnd2  15506  lbspss  21082  lindff1  21840  islinds4  21855  mdetunilem9  22636  madutpos  22658  neiptopnei  23150  mbflimsup  25709  cxpneg  26731  cxpmul2  26739  cxpsqrt  26753  cxpaddd  26767  cxpsubd  26768  divcxpd  26772  fsumharmonic  27063  bposlem1  27336  lgsqr  27403  chpchtlim  27531  sltmul2d  28196  ax5seg  28895  archiabllem2c  33101  qsidomlem2  33373  dimlssid  33572  logdivsqrle  34554  lindsadd  37381  lshpnelb  38749  cdlemg2fv2  40366  cdlemg2m  40370  cdlemg9a  40398  cdlemg9b  40399  cdlemg12b  40410  cdlemg14f  40419  cdlemg14g  40420  cdlemg17dN  40429  cdlemkj  40629  cdlemkuv2  40633  cdlemk52  40720  cdlemk53a  40721  mullimc  45327  mullimcf  45334  sfprmdvdsmersenne  47265  lincfsuppcl  47897