Theorem syl211anc 1384

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  syl212anc  1388  syl221anc  1389  frrlem15  9679  supicc  13452  modaddmulmod  13898  limsupgre  15441  limsupbnd1  15442  limsupbnd2  15443  lbspss  21079  lindff1  21802  islinds4  21817  mdetunilem9  22610  madutpos  22632  neiptopnei  23122  mbflimsup  25658  cxpneg  26670  cxpmul2  26678  cxpsqrt  26692  cxpaddd  26706  cxpsubd  26707  divcxpd  26711  fsumharmonic  27000  bposlem1  27272  lgsqr  27339  chpchtlim  27467  ltmuls2d  28189  ax5seg  29032  archiabllem2c  33283  qsidomlem2  33543  selvply1rhmlemb  33710  dimlssid  33823  logdivsqrle  34841  lindsadd  37987  lshpnelb  39483  cdlemg2fv2  41099  cdlemg2m  41103  cdlemg9a  41131  cdlemg9b  41132  cdlemg12b  41143  cdlemg14f  41152  cdlemg14g  41153  cdlemg17dN  41162  cdlemkj  41362  cdlemkuv2  41366  cdlemk52  41453  cdlemk53a  41454  mullimc  46068  mullimcf  46075  sfprmdvdsmersenne  48088  lincfsuppcl  48911