Theorem syl211anc 1375

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 1370	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 396  df-3an 1088

This theorem is referenced by:  syl212anc  1379  syl221anc  1380  frrlem15  9755  supicc  13483  modaddmulmod  13908  limsupgre  15430  limsupbnd1  15431  limsupbnd2  15432  lbspss  20838  lindff1  21595  islinds4  21610  mdetunilem9  22343  madutpos  22365  neiptopnei  22857  mbflimsup  25416  cxpneg  26422  cxpmul2  26430  cxpsqrt  26444  cxpaddd  26458  cxpsubd  26459  divcxpd  26463  fsumharmonic  26749  bposlem1  27020  lgsqr  27087  chpchtlim  27215  sltmul2d  27860  ax5seg  28460  archiabllem2c  32608  qsidomlem2  32843  logdivsqrle  33957  lindsadd  36785  lshpnelb  38158  cdlemg2fv2  39775  cdlemg2m  39779  cdlemg9a  39807  cdlemg9b  39808  cdlemg12b  39819  cdlemg14f  39828  cdlemg14g  39829  cdlemg17dN  39838  cdlemkj  40038  cdlemkuv2  40042  cdlemk52  40129  cdlemk53a  40130  mullimc  44632  mullimcf  44639  sfprmdvdsmersenne  46571  lincfsuppcl  47183