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  9657  supicc  13403  modaddmulmod  13847  limsupgre  15390  limsupbnd1  15391  limsupbnd2  15392  lbspss  21018  lindff1  21759  islinds4  21774  mdetunilem9  22536  madutpos  22558  neiptopnei  23048  mbflimsup  25595  cxpneg  26618  cxpmul2  26626  cxpsqrt  26640  cxpaddd  26654  cxpsubd  26655  divcxpd  26659  fsumharmonic  26950  bposlem1  27223  lgsqr  27290  chpchtlim  27418  sltmul2d  28112  ax5seg  28918  archiabllem2c  33171  qsidomlem2  33425  dimlssid  33666  logdivsqrle  34684  lindsadd  37674  lshpnelb  39104  cdlemg2fv2  40720  cdlemg2m  40724  cdlemg9a  40752  cdlemg9b  40753  cdlemg12b  40764  cdlemg14f  40773  cdlemg14g  40774  cdlemg17dN  40783  cdlemkj  40983  cdlemkuv2  40987  cdlemk52  41074  cdlemk53a  41075  mullimc  45741  mullimcf  45748  sfprmdvdsmersenne  47728  lincfsuppcl  48539