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  13454  modaddmulmod  13900  limsupgre  15443  limsupbnd1  15444  limsupbnd2  15445  lbspss  21077  lindff1  21800  islinds4  21815  mdetunilem9  22585  madutpos  22607  neiptopnei  23097  mbflimsup  25633  cxpneg  26645  cxpmul2  26653  cxpsqrt  26667  cxpaddd  26681  cxpsubd  26682  divcxpd  26686  fsumharmonic  26975  bposlem1  27247  lgsqr  27314  chpchtlim  27442  ltmuls2d  28164  ax5seg  29007  archiabllem2c  33256  qsidomlem2  33513  dimlssid  33776  logdivsqrle  34794  lindsadd  37934  lshpnelb  39430  cdlemg2fv2  41046  cdlemg2m  41050  cdlemg9a  41078  cdlemg9b  41079  cdlemg12b  41090  cdlemg14f  41099  cdlemg14g  41100  cdlemg17dN  41109  cdlemkj  41309  cdlemkuv2  41313  cdlemk52  41400  cdlemk53a  41401  mullimc  46046  mullimcf  46053  sfprmdvdsmersenne  48066  lincfsuppcl  48889