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 511	. 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 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  syl212anc  1382  syl221anc  1383  frrlem15  9669  supicc  13417  modaddmulmod  13861  limsupgre  15404  limsupbnd1  15405  limsupbnd2  15406  lbspss  21034  lindff1  21775  islinds4  21790  mdetunilem9  22564  madutpos  22586  neiptopnei  23076  mbflimsup  25623  cxpneg  26646  cxpmul2  26654  cxpsqrt  26668  cxpaddd  26682  cxpsubd  26683  divcxpd  26687  fsumharmonic  26978  bposlem1  27251  lgsqr  27318  chpchtlim  27446  ltmuls2d  28168  ax5seg  29011  archiabllem2c  33277  qsidomlem2  33534  dimlssid  33789  logdivsqrle  34807  lindsadd  37810  lshpnelb  39240  cdlemg2fv2  40856  cdlemg2m  40860  cdlemg9a  40888  cdlemg9b  40889  cdlemg12b  40900  cdlemg14f  40909  cdlemg14g  40910  cdlemg17dN  40919  cdlemkj  41119  cdlemkuv2  41123  cdlemk52  41210  cdlemk53a  41211  mullimc  45858  mullimcf  45865  sfprmdvdsmersenne  47845  lincfsuppcl  48655