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  9710  supicc  13462  modaddmulmod  13903  limsupgre  15447  limsupbnd1  15448  limsupbnd2  15449  lbspss  20989  lindff1  21729  islinds4  21744  mdetunilem9  22507  madutpos  22529  neiptopnei  23019  mbflimsup  25567  cxpneg  26590  cxpmul2  26598  cxpsqrt  26612  cxpaddd  26626  cxpsubd  26627  divcxpd  26631  fsumharmonic  26922  bposlem1  27195  lgsqr  27262  chpchtlim  27390  sltmul2d  28075  ax5seg  28865  archiabllem2c  33149  qsidomlem2  33424  dimlssid  33628  logdivsqrle  34641  lindsadd  37607  lshpnelb  38977  cdlemg2fv2  40594  cdlemg2m  40598  cdlemg9a  40626  cdlemg9b  40627  cdlemg12b  40638  cdlemg14f  40647  cdlemg14g  40648  cdlemg17dN  40657  cdlemkj  40857  cdlemkuv2  40861  cdlemk52  40948  cdlemk53a  40949  mullimc  45614  mullimcf  45621  sfprmdvdsmersenne  47604  lincfsuppcl  48402