Theorem syl211anc 1399

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 520	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
5		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
6		syl211anc.5	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) → 𝜂)
7	3, 4, 5, 6	syl3anc 1394	1 ⊢ (𝜑 → 𝜂)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  syl212anc  1403  syl221anc  1404  frrlem15  9717  supicc  13519  modaddmulmod  13965  limsupgre  15522  limsupbnd1  15523  limsupbnd2  15524  lbspss  21172  qsidomlem2  21441  lindff1  21930  islinds4  21945  mdetunilem9  22738  madutpos  22760  neiptopnei  23250  mbflimsup  25786  cxpneg  26804  cxpmul2  26812  cxpsqrt  26826  cxpaddd  26840  cxpsubd  26841  divcxpd  26845  fsumharmonic  27134  bposlem1  27406  lgsqr  27473  chpchtlim  27601  ltmuls2d  28323  ax5seg  29197  archiabllem2c  33428  selvply1rhmlemb  33826  dimlssid  33939  logdivsqrle  34954  lindsadd  38124  lshpnelb  39620  cdlemg2fv2  41236  cdlemg2m  41240  cdlemg9a  41268  cdlemg9b  41269  cdlemg12b  41280  cdlemg14f  41289  cdlemg14g  41290  cdlemg17dN  41299  cdlemkj  41499  cdlemkuv2  41503  cdlemk52  41590  cdlemk53a  41591  mullimc  46190  mullimcf  46197  sfprmdvdsmersenne  48210  lincfsuppcl  49044