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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl212anc  1407  syl221anc  1408  frrlem15  9764  supicc  13635  modaddmulmod  14084  limsupgre  15653  limsupbnd1  15654  limsupbnd2  15655  lbspss  21362  qsidomlem2  21642  lindff1  22131  islinds4  22146  mdetunilem9  22940  madutpos  22962  neiptopnei  23455  mbflimsup  25992  cxpneg  27014  cxpmul2  27022  cxpsqrt  27036  cxpaddd  27050  cxpsubd  27051  divcxpd  27055  fsumharmonic  27344  bposlem1  27616  lgsqr  27683  chpchtlim  27811  ltmuls2d  28563  ax5seg  29521  archiabllem2c  33802  selvply1rhmlemb  34197  dimlssid  34310  logdivsqrle  35325  lindsadd  38629  lshpnelb  40134  cdlemg2fv2  41750  cdlemg2m  41754  cdlemg9a  41782  cdlemg9b  41783  cdlemg12b  41794  cdlemg14f  41803  cdlemg14g  41804  cdlemg17dN  41813  cdlemkj  42013  cdlemkuv2  42017  cdlemk52  42104  cdlemk53a  42105  mullimc  46721  mullimcf  46728  squeezedltsq  48005  sfprmdvdsmersenne  48781  lincfsuppcl  49618