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  9743  supicc  13558  modaddmulmod  14006  limsupgre  15572  limsupbnd1  15573  limsupbnd2  15574  lbspss  21272  qsidomlem2  21550  lindff1  22039  islinds4  22054  mdetunilem9  22848  madutpos  22870  neiptopnei  23363  mbflimsup  25900  cxpneg  26926  cxpmul2  26934  cxpsqrt  26948  cxpaddd  26962  cxpsubd  26963  divcxpd  26967  fsumharmonic  27256  bposlem1  27528  lgsqr  27595  chpchtlim  27723  ltmuls2d  28445  ax5seg  29403  archiabllem2c  33643  selvply1rhmlemb  34037  dimlssid  34150  logdivsqrle  35166  lindsadd  38375  lshpnelb  39865  cdlemg2fv2  41481  cdlemg2m  41485  cdlemg9a  41513  cdlemg9b  41514  cdlemg12b  41525  cdlemg14f  41534  cdlemg14g  41535  cdlemg17dN  41544  cdlemkj  41744  cdlemkuv2  41748  cdlemk52  41835  cdlemk53a  41836  mullimc  46454  mullimcf  46461  squeezedltsq  47738  sfprmdvdsmersenne  48514  lincfsuppcl  49351