Theorem syl211anc 1372

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  syl212anc  1376  syl221anc  1377  supicc  12885  modaddmulmod  13305  limsupgre  14837  limsupbnd1  14838  limsupbnd2  14839  lbspss  19853  lindff1  20963  islinds4  20978  mdetunilem9  21228  madutpos  21250  neiptopnei  21739  mbflimsup  24266  cxpneg  25263  cxpmul2  25271  cxpsqrt  25285  cxpaddd  25299  cxpsubd  25300  divcxpd  25304  fsumharmonic  25588  bposlem1  25859  lgsqr  25926  chpchtlim  26054  ax5seg  26723  archiabllem2c  30824  qsidomlem2  30966  logdivsqrle  31921  frrlem15  33142  lindsadd  34884  lshpnelb  36119  cdlemg2fv2  37735  cdlemg2m  37739  cdlemg9a  37767  cdlemg9b  37768  cdlemg12b  37779  cdlemg14f  37788  cdlemg14g  37789  cdlemg17dN  37798  cdlemkj  37998  cdlemkuv2  38002  cdlemk52  38089  cdlemk53a  38090  mullimc  41895  mullimcf  41902  sfprmdvdsmersenne  43767  lincfsuppcl  44467