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  9771  supicc  13518  modaddmulmod  13956  limsupgre  15497  limsupbnd1  15498  limsupbnd2  15499  lbspss  21040  lindff1  21780  islinds4  21795  mdetunilem9  22558  madutpos  22580  neiptopnei  23070  mbflimsup  25619  cxpneg  26642  cxpmul2  26650  cxpsqrt  26664  cxpaddd  26678  cxpsubd  26679  divcxpd  26683  fsumharmonic  26974  bposlem1  27247  lgsqr  27314  chpchtlim  27442  sltmul2d  28127  ax5seg  28917  archiabllem2c  33193  qsidomlem2  33468  dimlssid  33672  logdivsqrle  34682  lindsadd  37637  lshpnelb  39002  cdlemg2fv2  40619  cdlemg2m  40623  cdlemg9a  40651  cdlemg9b  40652  cdlemg12b  40663  cdlemg14f  40672  cdlemg14g  40673  cdlemg17dN  40682  cdlemkj  40882  cdlemkuv2  40886  cdlemk52  40973  cdlemk53a  40974  mullimc  45645  mullimcf  45652  sfprmdvdsmersenne  47617  lincfsuppcl  48389