Theorem syl211anc 1403

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  syl212anc  1407  syl221anc  1408  frrlem15  9730  supicc  13529  modaddmulmod  13976  limsupgre  15534  limsupbnd1  15535  limsupbnd2  15536  lbspss  21184  qsidomlem2  21462  lindff1  21951  islinds4  21966  mdetunilem9  22758  madutpos  22780  neiptopnei  23270  mbflimsup  25806  cxpneg  26824  cxpmul2  26832  cxpsqrt  26846  cxpaddd  26860  cxpsubd  26861  divcxpd  26865  fsumharmonic  27154  bposlem1  27426  lgsqr  27493  chpchtlim  27621  ltmuls2d  28343  ax5seg  29266  archiabllem2c  33493  selvply1rhmlemb  33887  dimlssid  34000  logdivsqrle  35015  lindsadd  38242  lshpnelb  39736  cdlemg2fv2  41352  cdlemg2m  41356  cdlemg9a  41384  cdlemg9b  41385  cdlemg12b  41396  cdlemg14f  41405  cdlemg14g  41406  cdlemg17dN  41415  cdlemkj  41615  cdlemkuv2  41619  cdlemk52  41706  cdlemk53a  41707  mullimc  46312  mullimcf  46319  sfprmdvdsmersenne  48332  lincfsuppcl  49170