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  9672  supicc  13445  modaddmulmod  13891  limsupgre  15434  limsupbnd1  15435  limsupbnd2  15436  lbspss  21069  lindff1  21810  islinds4  21825  mdetunilem9  22595  madutpos  22617  neiptopnei  23107  mbflimsup  25643  cxpneg  26658  cxpmul2  26666  cxpsqrt  26680  cxpaddd  26694  cxpsubd  26695  divcxpd  26699  fsumharmonic  26989  bposlem1  27261  lgsqr  27328  chpchtlim  27456  ltmuls2d  28178  ax5seg  29021  archiabllem2c  33271  qsidomlem2  33528  dimlssid  33792  logdivsqrle  34810  lindsadd  37948  lshpnelb  39444  cdlemg2fv2  41060  cdlemg2m  41064  cdlemg9a  41092  cdlemg9b  41093  cdlemg12b  41104  cdlemg14f  41113  cdlemg14g  41114  cdlemg17dN  41123  cdlemkj  41323  cdlemkuv2  41327  cdlemk52  41414  cdlemk53a  41415  mullimc  46064  mullimcf  46071  sfprmdvdsmersenne  48078  lincfsuppcl  48901