Theorem syl211anc 1374

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 1369	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  syl212anc  1378  syl221anc  1379  frrlem15  9775  supicc  13505  modaddmulmod  13930  limsupgre  15452  limsupbnd1  15453  limsupbnd2  15454  lbspss  20961  lindff1  21748  islinds4  21763  mdetunilem9  22516  madutpos  22538  neiptopnei  23030  mbflimsup  25589  cxpneg  26609  cxpmul2  26617  cxpsqrt  26631  cxpaddd  26645  cxpsubd  26646  divcxpd  26650  fsumharmonic  26938  bposlem1  27211  lgsqr  27278  chpchtlim  27406  sltmul2d  28066  ax5seg  28743  archiabllem2c  32898  qsidomlem2  33164  logdivsqrle  34277  lindsadd  37081  lshpnelb  38451  cdlemg2fv2  40068  cdlemg2m  40072  cdlemg9a  40100  cdlemg9b  40101  cdlemg12b  40112  cdlemg14f  40121  cdlemg14g  40122  cdlemg17dN  40131  cdlemkj  40331  cdlemkuv2  40335  cdlemk52  40422  cdlemk53a  40423  mullimc  44995  mullimcf  45002  sfprmdvdsmersenne  46934  lincfsuppcl  47472