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 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  1382  syl221anc  1383  frrlem15  9797  supicc  13541  modaddmulmod  13979  limsupgre  15517  limsupbnd1  15518  limsupbnd2  15519  lbspss  21081  lindff1  21840  islinds4  21855  mdetunilem9  22626  madutpos  22648  neiptopnei  23140  mbflimsup  25701  cxpneg  26723  cxpmul2  26731  cxpsqrt  26745  cxpaddd  26759  cxpsubd  26760  divcxpd  26764  fsumharmonic  27055  bposlem1  27328  lgsqr  27395  chpchtlim  27523  sltmul2d  28198  ax5seg  28953  archiabllem2c  33202  qsidomlem2  33481  dimlssid  33683  logdivsqrle  34665  lindsadd  37620  lshpnelb  38985  cdlemg2fv2  40602  cdlemg2m  40606  cdlemg9a  40634  cdlemg9b  40635  cdlemg12b  40646  cdlemg14f  40655  cdlemg14g  40656  cdlemg17dN  40665  cdlemkj  40865  cdlemkuv2  40869  cdlemk52  40956  cdlemk53a  40957  mullimc  45631  mullimcf  45638  sfprmdvdsmersenne  47590  lincfsuppcl  48330