Theorem syl211anc 1329

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl211anc.5	⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂)

Assertion

Ref	Expression
syl211anc	⊢ (𝜑 → 𝜂)

Proof of Theorem syl211anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 554	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl211anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂)
7	3, 4, 5, 6	syl3anc 1323	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036

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 197  df-an 386  df-3an 1038

This theorem is referenced by:  syl212anc  1333  syl221anc  1334  supicc  12259  modaddmulmod  12674  limsupgre  14141  limsupbnd1  14142  limsupbnd2  14143  lbspss  18996  lindff1  20073  islinds4  20088  mdetunilem9  20340  madutpos  20362  neiptopnei  20841  mbflimsup  23334  cxpneg  24322  cxpmul2  24330  cxpsqrt  24344  cxpaddd  24358  cxpsubd  24359  divcxpd  24363  fsumharmonic  24633  bposlem1  24904  lgsqr  24971  chpchtlim  25063  ax5seg  25713  archiabllem2c  29526  lshpnelb  33737  cdlemg2fv2  35354  cdlemg2m  35358  cdlemg9a  35386  cdlemg9b  35387  cdlemg12b  35398  cdlemg14f  35407  cdlemg14g  35408  cdlemg17dN  35417  cdlemkj  35617  cdlemkuv2  35621  cdlemk52  35708  cdlemk53a  35709  mullimc  39239  mullimcf  39246  sfprmdvdsmersenne  40807  lincfsuppcl  41464