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  9647  supicc  13398  modaddmulmod  13842  limsupgre  15385  limsupbnd1  15386  limsupbnd2  15387  lbspss  21014  lindff1  21755  islinds4  21770  mdetunilem9  22533  madutpos  22555  neiptopnei  23045  mbflimsup  25592  cxpneg  26615  cxpmul2  26623  cxpsqrt  26637  cxpaddd  26651  cxpsubd  26652  divcxpd  26656  fsumharmonic  26947  bposlem1  27220  lgsqr  27287  chpchtlim  27415  sltmul2d  28109  ax5seg  28914  archiabllem2c  33159  qsidomlem2  33413  dimlssid  33640  logdivsqrle  34658  lindsadd  37652  lshpnelb  39022  cdlemg2fv2  40638  cdlemg2m  40642  cdlemg9a  40670  cdlemg9b  40671  cdlemg12b  40682  cdlemg14f  40691  cdlemg14g  40692  cdlemg17dN  40701  cdlemkj  40901  cdlemkuv2  40905  cdlemk52  40992  cdlemk53a  40993  mullimc  45655  mullimcf  45662  sfprmdvdsmersenne  47633  lincfsuppcl  48444