Theorem syl211anc 1375

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

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

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  syl212anc  1379  syl221anc  1380  frrlem15  9515  supicc  13233  modaddmulmod  13658  limsupgre  15190  limsupbnd1  15191  limsupbnd2  15192  lbspss  20344  lindff1  21027  islinds4  21042  mdetunilem9  21769  madutpos  21791  neiptopnei  22283  mbflimsup  24830  cxpneg  25836  cxpmul2  25844  cxpsqrt  25858  cxpaddd  25872  cxpsubd  25873  divcxpd  25877  fsumharmonic  26161  bposlem1  26432  lgsqr  26499  chpchtlim  26627  ax5seg  27306  archiabllem2c  31449  qsidomlem2  31629  logdivsqrle  32630  lindsadd  35770  lshpnelb  36998  cdlemg2fv2  38614  cdlemg2m  38618  cdlemg9a  38646  cdlemg9b  38647  cdlemg12b  38658  cdlemg14f  38667  cdlemg14g  38668  cdlemg17dN  38677  cdlemkj  38877  cdlemkuv2  38881  cdlemk52  38968  cdlemk53a  38969  mullimc  43157  mullimcf  43164  sfprmdvdsmersenne  45055  lincfsuppcl  45754