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  9717  supicc  13469  modaddmulmod  13910  limsupgre  15454  limsupbnd1  15455  limsupbnd2  15456  lbspss  20996  lindff1  21736  islinds4  21751  mdetunilem9  22514  madutpos  22536  neiptopnei  23026  mbflimsup  25574  cxpneg  26597  cxpmul2  26605  cxpsqrt  26619  cxpaddd  26633  cxpsubd  26634  divcxpd  26638  fsumharmonic  26929  bposlem1  27202  lgsqr  27269  chpchtlim  27397  sltmul2d  28082  ax5seg  28872  archiabllem2c  33156  qsidomlem2  33431  dimlssid  33635  logdivsqrle  34648  lindsadd  37614  lshpnelb  38984  cdlemg2fv2  40601  cdlemg2m  40605  cdlemg9a  40633  cdlemg9b  40634  cdlemg12b  40645  cdlemg14f  40654  cdlemg14g  40655  cdlemg17dN  40664  cdlemkj  40864  cdlemkuv2  40868  cdlemk52  40955  cdlemk53a  40956  mullimc  45621  mullimcf  45628  sfprmdvdsmersenne  47608  lincfsuppcl  48406