Theorem syl222anc 1413

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

Hypotheses

Ref	Expression
syl3anc.1	⊢ (𝜑 → 𝜓)
syl3anc.2	⊢ (𝜑 → 𝜒)
syl3anc.3	⊢ (𝜑 → 𝜃)
syl3Xanc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl33anc.6	⊢ (𝜑 → 𝜁)
syl222anc.7	⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)

Assertion

Ref	Expression
syl222anc	⊢ (𝜑 → 𝜎)

Proof of Theorem syl222anc

Step	Hyp	Ref	Expression
1		syl3anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl3anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl3anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl3Xanc.4	. 2 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6		syl33anc.6	. . 3 ⊢ (𝜑 → 𝜁)
7	5, 6	jca 520	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁))
8		syl222anc.7	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)
9	1, 2, 3, 4, 7, 8	syl221anc 1408	1 ⊢ (𝜑 → 𝜎)

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

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 1105

This theorem is referenced by:  3anandis  1500  3anandirs  1501  omopth2  8570  omeu  8571  dfac12lem2  10129  xaddass2  13277  xpncan  13278  divdenle  16809  pockthlem  16966  znidomb  21692  tanord1  26683  ang180lem5  26959  isosctrlem3  26966  log2tlbnd  27091  basellem1  27226  perfectlem2  27375  bposlem6  27434  dchrisum0flblem2  27654  pntpbnd1a  27730  mulsproplem1  28290  axcontlem8  29302  xlt2addrd  33085  s2f1  33246  xrge0addass  33317  xrge0npcan  33321  elrgspnlem1  33543  submatminr1  34181  carsgclctunlem2  34690  nmulss1  36672  4atexlemntlpq  40823  4atexlemnclw  40825  trlval2  40918  cdleme0moN  40980  cdleme16b  41034  cdleme16c  41035  cdleme16d  41036  cdleme16e  41037  cdleme17c  41043  cdlemeda  41053  cdleme20h  41071  cdleme20j  41073  cdleme20l2  41076  cdleme21c  41082  cdleme21ct  41084  cdleme22aa  41094  cdleme22cN  41097  cdleme22d  41098  cdleme22e  41099  cdleme22eALTN  41100  cdleme23b  41105  cdleme25a  41108  cdleme25dN  41111  cdleme27N  41124  cdleme28a  41125  cdleme28b  41126  cdleme29ex  41129  cdleme32c  41198  cdleme42k  41239  cdlemg2cex  41346  cdlemg2idN  41351  cdlemg31c  41454  cdlemk5a  41590  cdlemk5  41591  congmul  43677  jm2.25lem1  43708  jm2.26  43712  jm2.27a  43715  infleinflem1  46068  stoweidlem42  46739