Theorem syl211anc 1378

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 1373	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  1382  syl221anc  1383  frrlem15  9653  supicc  13404  modaddmulmod  13845  limsupgre  15388  limsupbnd1  15389  limsupbnd2  15390  lbspss  20986  lindff1  21727  islinds4  21742  mdetunilem9  22505  madutpos  22527  neiptopnei  23017  mbflimsup  25565  cxpneg  26588  cxpmul2  26596  cxpsqrt  26610  cxpaddd  26624  cxpsubd  26625  divcxpd  26629  fsumharmonic  26920  bposlem1  27193  lgsqr  27260  chpchtlim  27388  sltmul2d  28080  ax5seg  28883  archiabllem2c  33138  qsidomlem2  33391  dimlssid  33605  logdivsqrle  34624  lindsadd  37603  lshpnelb  38973  cdlemg2fv2  40589  cdlemg2m  40593  cdlemg9a  40621  cdlemg9b  40622  cdlemg12b  40633  cdlemg14f  40642  cdlemg14g  40643  cdlemg17dN  40652  cdlemkj  40852  cdlemkuv2  40856  cdlemk52  40943  cdlemk53a  40944  mullimc  45607  mullimcf  45614  sfprmdvdsmersenne  47597  lincfsuppcl  48408