Theorem syl211anc 1403

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 1398	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  1407  syl221anc  1408  frrlem15  9742  supicc  13556  modaddmulmod  14004  limsupgre  15570  limsupbnd1  15571  limsupbnd2  15572  lbspss  21267  qsidomlem2  21545  lindff1  22034  islinds4  22049  mdetunilem9  22843  madutpos  22865  neiptopnei  23358  mbflimsup  25895  cxpneg  26916  cxpmul2  26924  cxpsqrt  26938  cxpaddd  26952  cxpsubd  26953  divcxpd  26957  fsumharmonic  27246  bposlem1  27518  lgsqr  27585  chpchtlim  27713  ltmuls2d  28435  ax5seg  29381  archiabllem2c  33622  selvply1rhmlemb  34016  dimlssid  34129  logdivsqrle  35145  lindsadd  38354  lshpnelb  39844  cdlemg2fv2  41460  cdlemg2m  41464  cdlemg9a  41492  cdlemg9b  41493  cdlemg12b  41504  cdlemg14f  41513  cdlemg14g  41514  cdlemg17dN  41523  cdlemkj  41723  cdlemkuv2  41727  cdlemk52  41814  cdlemk53a  41815  mullimc  46433  mullimcf  46440  squeezedltsq  47717  sfprmdvdsmersenne  48493  lincfsuppcl  49330