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  9754  supicc  13480  modaddmulmod  13905  limsupgre  15427  limsupbnd1  15428  limsupbnd2  15429  lbspss  20698  lindff1  21381  islinds4  21396  mdetunilem9  22129  madutpos  22151  neiptopnei  22643  mbflimsup  25190  cxpneg  26196  cxpmul2  26204  cxpsqrt  26218  cxpaddd  26232  cxpsubd  26233  divcxpd  26237  fsumharmonic  26523  bposlem1  26794  lgsqr  26861  chpchtlim  26989  sltmul2d  27634  ax5seg  28234  archiabllem2c  32382  qsidomlem2  32617  logdivsqrle  33731  lindsadd  36567  lshpnelb  37940  cdlemg2fv2  39557  cdlemg2m  39561  cdlemg9a  39589  cdlemg9b  39590  cdlemg12b  39601  cdlemg14f  39610  cdlemg14g  39611  cdlemg17dN  39620  cdlemkj  39820  cdlemkuv2  39824  cdlemk52  39911  cdlemk53a  39912  mullimc  44411  mullimcf  44418  sfprmdvdsmersenne  46350  lincfsuppcl  47172