Theorem syl211anc 1324

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl211anc.5	⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂)

Assertion

Ref	Expression
syl211anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl211anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 553	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl211anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂)
7	3, 4, 5, 6	syl3anc 1318	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  syl212anc  1328  syl221anc  1329  supicc  12191  modaddmulmod  12599  limsupgre  14060  limsupbnd1  14061  limsupbnd2  14062  lbspss  18903  lindff1  19978  islinds4  19993  mdetunilem9  20245  madutpos  20267  neiptopnei  20746  mbflimsup  23239  cxpneg  24227  cxpmul2  24235  cxpsqrt  24249  cxpaddd  24263  cxpsubd  24264  divcxpd  24268  fsumharmonic  24538  bposlem1  24809  lgsqr  24876  chpchtlim  24968  ax5seg  25618  archiabllem2c  29080  lshpnelb  33289  cdlemg2fv2  34906  cdlemg2m  34910  cdlemg9a  34938  cdlemg9b  34939  cdlemg12b  34950  cdlemg14f  34959  cdlemg14g  34960  cdlemg17dN  34969  cdlemkj  35169  cdlemkuv2  35173  cdlemk52  35260  cdlemk53a  35261  mullimc  38683  mullimcf  38690  sfprmdvdsmersenne  40058  lincfsuppcl  41996