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 511	. 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 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  syl212anc  1380  syl221anc  1381  frrlem15  9826  supicc  13561  modaddmulmod  13989  limsupgre  15527  limsupbnd1  15528  limsupbnd2  15529  lbspss  21104  lindff1  21863  islinds4  21878  mdetunilem9  22647  madutpos  22669  neiptopnei  23161  mbflimsup  25720  cxpneg  26741  cxpmul2  26749  cxpsqrt  26763  cxpaddd  26777  cxpsubd  26778  divcxpd  26782  fsumharmonic  27073  bposlem1  27346  lgsqr  27413  chpchtlim  27541  sltmul2d  28216  ax5seg  28971  archiabllem2c  33175  qsidomlem2  33446  dimlssid  33645  logdivsqrle  34627  lindsadd  37573  lshpnelb  38940  cdlemg2fv2  40557  cdlemg2m  40561  cdlemg9a  40589  cdlemg9b  40590  cdlemg12b  40601  cdlemg14f  40610  cdlemg14g  40611  cdlemg17dN  40620  cdlemkj  40820  cdlemkuv2  40824  cdlemk52  40911  cdlemk53a  40912  mullimc  45537  mullimcf  45544  sfprmdvdsmersenne  47477  lincfsuppcl  48142