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  9739  supicc  13546  modaddmulmod  13994  limsupgre  15558  limsupbnd1  15559  limsupbnd2  15560  lbspss  21240  qsidomlem2  21518  lindff1  22007  islinds4  22022  mdetunilem9  22814  madutpos  22836  neiptopnei  23326  mbflimsup  25862  cxpneg  26883  cxpmul2  26891  cxpsqrt  26905  cxpaddd  26919  cxpsubd  26920  divcxpd  26924  fsumharmonic  27213  bposlem1  27485  lgsqr  27552  chpchtlim  27680  ltmuls2d  28402  ax5seg  29325  archiabllem2c  33546  selvply1rhmlemb  33940  dimlssid  34053  logdivsqrle  35069  lindsadd  38305  lshpnelb  39799  cdlemg2fv2  41415  cdlemg2m  41419  cdlemg9a  41447  cdlemg9b  41448  cdlemg12b  41459  cdlemg14f  41468  cdlemg14g  41469  cdlemg17dN  41478  cdlemkj  41678  cdlemkuv2  41682  cdlemk52  41769  cdlemk53a  41770  mullimc  46373  mullimcf  46380  sfprmdvdsmersenne  48396  lincfsuppcl  49234