Theorem syl211anc 1379

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 1374	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  1383  syl221anc  1384  frrlem15  9681  supicc  13429  modaddmulmod  13873  limsupgre  15416  limsupbnd1  15417  limsupbnd2  15418  lbspss  21046  lindff1  21787  islinds4  21802  mdetunilem9  22576  madutpos  22598  neiptopnei  23088  mbflimsup  25635  cxpneg  26658  cxpmul2  26666  cxpsqrt  26680  cxpaddd  26694  cxpsubd  26695  divcxpd  26699  fsumharmonic  26990  bposlem1  27263  lgsqr  27330  chpchtlim  27458  ltmuls2d  28180  ax5seg  29023  archiabllem2c  33288  qsidomlem2  33545  dimlssid  33809  logdivsqrle  34827  lindsadd  37858  lshpnelb  39354  cdlemg2fv2  40970  cdlemg2m  40974  cdlemg9a  41002  cdlemg9b  41003  cdlemg12b  41014  cdlemg14f  41023  cdlemg14g  41024  cdlemg17dN  41033  cdlemkj  41233  cdlemkuv2  41237  cdlemk52  41324  cdlemk53a  41325  mullimc  45970  mullimcf  45977  sfprmdvdsmersenne  47957  lincfsuppcl  48767