Theorem syl211anc 1404

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl212anc  1408  syl221anc  1409  frrlem15  9788  supicc  13659  modaddmulmod  14108  limsupgre  15677  limsupbnd1  15678  limsupbnd2  15679  lbspss  21387  qsidomlem2  21667  lindff1  22156  islinds4  22171  mdetunilem9  22965  madutpos  22987  neiptopnei  23480  mbflimsup  26017  cxpneg  27039  cxpmul2  27047  cxpsqrt  27061  cxpaddd  27075  cxpsubd  27076  divcxpd  27080  fsumharmonic  27369  bposlem1  27641  lgsqr  27708  chpchtlim  27836  ltmuls2d  28588  ax5seg  29546  archiabllem2c  33826  selvply1rhmlemb  34221  dimlssid  34334  logdivsqrle  35349  lindsadd  38728  lshpnelb  40233  cdlemg2fv2  41849  cdlemg2m  41853  cdlemg9a  41881  cdlemg9b  41882  cdlemg12b  41893  cdlemg14f  41902  cdlemg14g  41903  cdlemg17dN  41912  cdlemkj  42112  cdlemkuv2  42116  cdlemk52  42203  cdlemk53a  42204  mullimc  46833  mullimcf  46840  squeezedltsq  48117  sfprmdvdsmersenne  48893  lincfsuppcl  49730