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 515	. 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 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  syl212anc  1382  syl221anc  1383  frrlem15  9373  supicc  13089  modaddmulmod  13511  limsupgre  15042  limsupbnd1  15043  limsupbnd2  15044  lbspss  20119  lindff1  20782  islinds4  20797  mdetunilem9  21517  madutpos  21539  neiptopnei  22029  mbflimsup  24563  cxpneg  25569  cxpmul2  25577  cxpsqrt  25591  cxpaddd  25605  cxpsubd  25606  divcxpd  25610  fsumharmonic  25894  bposlem1  26165  lgsqr  26232  chpchtlim  26360  ax5seg  27029  archiabllem2c  31168  qsidomlem2  31343  logdivsqrle  32342  lindsadd  35507  lshpnelb  36735  cdlemg2fv2  38351  cdlemg2m  38355  cdlemg9a  38383  cdlemg9b  38384  cdlemg12b  38395  cdlemg14f  38404  cdlemg14g  38405  cdlemg17dN  38414  cdlemkj  38614  cdlemkuv2  38618  cdlemk52  38705  cdlemk53a  38706  mullimc  42832  mullimcf  42839  sfprmdvdsmersenne  44728  lincfsuppcl  45427