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  9446  supicc  13162  modaddmulmod  13586  limsupgre  15118  limsupbnd1  15119  limsupbnd2  15120  lbspss  20259  lindff1  20937  islinds4  20952  mdetunilem9  21677  madutpos  21699  neiptopnei  22191  mbflimsup  24735  cxpneg  25741  cxpmul2  25749  cxpsqrt  25763  cxpaddd  25777  cxpsubd  25778  divcxpd  25782  fsumharmonic  26066  bposlem1  26337  lgsqr  26404  chpchtlim  26532  ax5seg  27209  archiabllem2c  31351  qsidomlem2  31531  logdivsqrle  32530  lindsadd  35697  lshpnelb  36925  cdlemg2fv2  38541  cdlemg2m  38545  cdlemg9a  38573  cdlemg9b  38574  cdlemg12b  38585  cdlemg14f  38594  cdlemg14g  38595  cdlemg17dN  38604  cdlemkj  38804  cdlemkuv2  38808  cdlemk52  38895  cdlemk53a  38896  mullimc  43047  mullimcf  43054  sfprmdvdsmersenne  44943  lincfsuppcl  45642