Theorem syl211anc 1413

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 555	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl211anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂)
7	3, 4, 5, 6	syl3anc 1407	1 ⊢ (𝜑 → 𝜂)

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

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  syl212anc  1417  syl221anc  1418  supicc  12402  modaddmulmod  12820  limsupgre  14300  limsupbnd1  14301  limsupbnd2  14302  lbspss  19173  lindff1  20250  islinds4  20265  mdetunilem9  20517  madutpos  20539  neiptopnei  21027  mbflimsup  23521  cxpneg  24515  cxpmul2  24523  cxpsqrt  24537  cxpaddd  24551  cxpsubd  24552  divcxpd  24556  fsumharmonic  24826  bposlem1  25097  lgsqr  25164  chpchtlim  25256  ax5seg  25906  archiabllem2c  29947  logdivsqrle  30926  lshpnelb  34659  cdlemg2fv2  36275  cdlemg2m  36279  cdlemg9a  36307  cdlemg9b  36308  cdlemg12b  36319  cdlemg14f  36328  cdlemg14g  36329  cdlemg17dN  36338  cdlemkj  36538  cdlemkuv2  36542  cdlemk52  36629  cdlemk53a  36630  mullimc  40236  mullimcf  40243  sfprmdvdsmersenne  41915  lincfsuppcl  42597