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  8548  omeu  8549  dfac12lem2  10098  xaddass2  13210  xpncan  13211  divdenle  16719  pockthlem  16876  znidomb  21471  tanord1  26446  ang180lem5  26723  isosctrlem3  26730  log2tlbnd  26855  basellem1  26991  perfectlem2  27141  bposlem6  27200  dchrisum0flblem2  27420  pntpbnd1a  27496  mulsproplem1  28019  axcontlem8  28898  xlt2addrd  32682  s2f1  32866  xrge0addass  32957  xrge0npcan  32961  elrgspnlem1  33193  submatminr1  33800  carsgclctunlem2  34310  4atexlemntlpq  40062  4atexlemnclw  40064  trlval2  40157  cdleme0moN  40219  cdleme16b  40273  cdleme16c  40274  cdleme16d  40275  cdleme16e  40276  cdleme17c  40282  cdlemeda  40292  cdleme20h  40310  cdleme20j  40312  cdleme20l2  40315  cdleme21c  40321  cdleme21ct  40323  cdleme22aa  40333  cdleme22cN  40336  cdleme22d  40337  cdleme22e  40338  cdleme22eALTN  40339  cdleme23b  40344  cdleme25a  40347  cdleme25dN  40350  cdleme27N  40363  cdleme28a  40364  cdleme28b  40365  cdleme29ex  40368  cdleme32c  40437  cdleme42k  40478  cdlemg2cex  40585  cdlemg2idN  40590  cdlemg31c  40693  cdlemk5a  40829  cdlemk5  40830  congmul  42956  jm2.25lem1  42987  jm2.26  42991  jm2.27a  42994  infleinflem1  45366  stoweidlem42  46040