Theorem syl211anc 1376

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  syl212anc  1380  syl221anc  1381  frrlem15  9702  supicc  13428  modaddmulmod  13853  limsupgre  15375  limsupbnd1  15376  limsupbnd2  15377  lbspss  20600  lindff1  21263  islinds4  21278  mdetunilem9  22006  madutpos  22028  neiptopnei  22520  mbflimsup  25067  cxpneg  26073  cxpmul2  26081  cxpsqrt  26095  cxpaddd  26109  cxpsubd  26110  divcxpd  26114  fsumharmonic  26398  bposlem1  26669  lgsqr  26736  chpchtlim  26864  ax5seg  27950  archiabllem2c  32101  qsidomlem2  32302  logdivsqrle  33352  lindsadd  36144  lshpnelb  37519  cdlemg2fv2  39136  cdlemg2m  39140  cdlemg9a  39168  cdlemg9b  39169  cdlemg12b  39180  cdlemg14f  39189  cdlemg14g  39190  cdlemg17dN  39199  cdlemkj  39399  cdlemkuv2  39403  cdlemk52  39490  cdlemk53a  39491  mullimc  43977  mullimcf  43984  sfprmdvdsmersenne  45915  lincfsuppcl  46614