Theorem syl211anc 1394

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 519	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl211anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂)
7	3, 4, 5, 6	syl3anc 1389	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  syl212anc  1398  syl221anc  1399  frrlem15  9712  supicc  13502  modaddmulmod  13948  limsupgre  15491  limsupbnd1  15492  limsupbnd2  15493  lbspss  21129  lindff1  21852  islinds4  21867  mdetunilem9  22660  madutpos  22682  neiptopnei  23172  mbflimsup  25708  cxpneg  26723  cxpmul2  26731  cxpsqrt  26745  cxpaddd  26759  cxpsubd  26760  divcxpd  26764  fsumharmonic  27053  bposlem1  27325  lgsqr  27392  chpchtlim  27520  ltmuls2d  28242  ax5seg  29085  archiabllem2c  33336  qsidomlem2  33601  selvply1rhmlemb  33777  dimlssid  33890  logdivsqrle  34908  lindsadd  38076  lshpnelb  39572  cdlemg2fv2  41188  cdlemg2m  41192  cdlemg9a  41220  cdlemg9b  41221  cdlemg12b  41232  cdlemg14f  41241  cdlemg14g  41242  cdlemg17dN  41251  cdlemkj  41451  cdlemkuv2  41455  cdlemk52  41542  cdlemk53a  41543  mullimc  46156  mullimcf  46163  sfprmdvdsmersenne  48176  lincfsuppcl  48999