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  9745  supicc  13613  modaddmulmod  14061  limsupgre  15628  limsupbnd1  15629  limsupbnd2  15630  lbspss  21337  qsidomlem2  21617  lindff1  22106  islinds4  22121  mdetunilem9  22915  madutpos  22937  neiptopnei  23430  mbflimsup  25967  cxpneg  26991  cxpmul2  26999  cxpsqrt  27013  cxpaddd  27027  cxpsubd  27028  divcxpd  27032  fsumharmonic  27321  bposlem1  27593  lgsqr  27660  chpchtlim  27788  ltmuls2d  28540  ax5seg  29498  archiabllem2c  33738  selvply1rhmlemb  34133  dimlssid  34246  logdivsqrle  35262  lindsadd  38504  lshpnelb  40009  cdlemg2fv2  41625  cdlemg2m  41629  cdlemg9a  41657  cdlemg9b  41658  cdlemg12b  41669  cdlemg14f  41678  cdlemg14g  41679  cdlemg17dN  41688  cdlemkj  41888  cdlemkuv2  41892  cdlemk52  41979  cdlemk53a  41980  mullimc  46572  mullimcf  46579  squeezedltsq  47856  sfprmdvdsmersenne  48632  lincfsuppcl  49469