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 511	. 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 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  syl212anc  1379  syl221anc  1380  frrlem15  9795  supicc  13538  modaddmulmod  13976  limsupgre  15514  limsupbnd1  15515  limsupbnd2  15516  lbspss  21099  lindff1  21858  islinds4  21873  mdetunilem9  22642  madutpos  22664  neiptopnei  23156  mbflimsup  25715  cxpneg  26738  cxpmul2  26746  cxpsqrt  26760  cxpaddd  26774  cxpsubd  26775  divcxpd  26779  fsumharmonic  27070  bposlem1  27343  lgsqr  27410  chpchtlim  27538  sltmul2d  28213  ax5seg  28968  archiabllem2c  33185  qsidomlem2  33461  dimlssid  33660  logdivsqrle  34644  lindsadd  37600  lshpnelb  38966  cdlemg2fv2  40583  cdlemg2m  40587  cdlemg9a  40615  cdlemg9b  40616  cdlemg12b  40627  cdlemg14f  40636  cdlemg14g  40637  cdlemg17dN  40646  cdlemkj  40846  cdlemkuv2  40850  cdlemk52  40937  cdlemk53a  40938  mullimc  45572  mullimcf  45579  sfprmdvdsmersenne  47528  lincfsuppcl  48259