Theorem syl211anc 1377

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  syl212anc  1381  syl221anc  1382  frrlem15  9747  supicc  13473  modaddmulmod  13898  limsupgre  15420  limsupbnd1  15421  limsupbnd2  15422  lbspss  20680  lindff1  21358  islinds4  21373  mdetunilem9  22103  madutpos  22125  neiptopnei  22617  mbflimsup  25164  cxpneg  26170  cxpmul2  26178  cxpsqrt  26192  cxpaddd  26206  cxpsubd  26207  divcxpd  26211  fsumharmonic  26495  bposlem1  26766  lgsqr  26833  chpchtlim  26961  sltmul2d  27603  ax5seg  28175  archiabllem2c  32318  qsidomlem2  32529  logdivsqrle  33599  lindsadd  36418  lshpnelb  37791  cdlemg2fv2  39408  cdlemg2m  39412  cdlemg9a  39440  cdlemg9b  39441  cdlemg12b  39452  cdlemg14f  39461  cdlemg14g  39462  cdlemg17dN  39471  cdlemkj  39671  cdlemkuv2  39675  cdlemk52  39762  cdlemk53a  39763  mullimc  44266  mullimcf  44273  sfprmdvdsmersenne  46205  lincfsuppcl  46995