Theorem syl211anc 1378

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

This theorem is referenced by:  syl212anc  1382  syl221anc  1383  frrlem15  9672  supicc  13422  modaddmulmod  13863  limsupgre  15406  limsupbnd1  15407  limsupbnd2  15408  lbspss  21004  lindff1  21745  islinds4  21760  mdetunilem9  22523  madutpos  22545  neiptopnei  23035  mbflimsup  25583  cxpneg  26606  cxpmul2  26614  cxpsqrt  26628  cxpaddd  26642  cxpsubd  26643  divcxpd  26647  fsumharmonic  26938  bposlem1  27211  lgsqr  27278  chpchtlim  27406  sltmul2d  28098  ax5seg  28901  archiabllem2c  33147  qsidomlem2  33400  dimlssid  33604  logdivsqrle  34617  lindsadd  37592  lshpnelb  38962  cdlemg2fv2  40579  cdlemg2m  40583  cdlemg9a  40611  cdlemg9b  40612  cdlemg12b  40623  cdlemg14f  40632  cdlemg14g  40633  cdlemg17dN  40642  cdlemkj  40842  cdlemkuv2  40846  cdlemk52  40933  cdlemk53a  40934  mullimc  45598  mullimcf  45605  sfprmdvdsmersenne  47588  lincfsuppcl  48399