Theorem syl222anc 1388

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 511	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁))
8		syl222anc.7	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)
9	1, 2, 3, 4, 7, 8	syl221anc 1383	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3anandis  1473  3anandirs  1474  omopth2  8596  omeu  8597  dfac12lem2  10159  xaddass2  13266  xpncan  13267  divdenle  16768  pockthlem  16925  znidomb  21522  tanord1  26498  ang180lem5  26775  isosctrlem3  26782  log2tlbnd  26907  basellem1  27043  perfectlem2  27193  bposlem6  27252  dchrisum0flblem2  27472  pntpbnd1a  27548  mulsproplem1  28071  axcontlem8  28950  xlt2addrd  32736  s2f1  32920  xrge0addass  33011  xrge0npcan  33015  elrgspnlem1  33237  submatminr1  33841  carsgclctunlem2  34351  4atexlemntlpq  40087  4atexlemnclw  40089  trlval2  40182  cdleme0moN  40244  cdleme16b  40298  cdleme16c  40299  cdleme16d  40300  cdleme16e  40301  cdleme17c  40307  cdlemeda  40317  cdleme20h  40335  cdleme20j  40337  cdleme20l2  40340  cdleme21c  40346  cdleme21ct  40348  cdleme22aa  40358  cdleme22cN  40361  cdleme22d  40362  cdleme22e  40363  cdleme22eALTN  40364  cdleme23b  40369  cdleme25a  40372  cdleme25dN  40375  cdleme27N  40388  cdleme28a  40389  cdleme28b  40390  cdleme29ex  40393  cdleme32c  40462  cdleme42k  40503  cdlemg2cex  40610  cdlemg2idN  40615  cdlemg31c  40718  cdlemk5a  40854  cdlemk5  40855  congmul  42991  jm2.25lem1  43022  jm2.26  43026  jm2.27a  43029  infleinflem1  45397  stoweidlem42  46071