Theorem syl222anc 1386

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3anandis  1471  3anandirs  1472  omopth2  8586  omeu  8587  dfac12lem2  10141  xaddass2  13231  xpncan  13232  divdenle  16687  pockthlem  16840  znidomb  21123  tanord1  26053  ang180lem5  26325  isosctrlem3  26332  log2tlbnd  26457  basellem1  26592  perfectlem2  26740  bposlem6  26799  dchrisum0flblem2  27019  pntpbnd1a  27095  mulsproplem1  27582  axcontlem8  28267  xlt2addrd  32009  s2f1  32149  xrge0addass  32229  xrge0npcan  32233  submatminr1  32859  carsgclctunlem2  33387  4atexlemntlpq  39025  4atexlemnclw  39027  trlval2  39120  cdleme0moN  39182  cdleme16b  39236  cdleme16c  39237  cdleme16d  39238  cdleme16e  39239  cdleme17c  39245  cdlemeda  39255  cdleme20h  39273  cdleme20j  39275  cdleme20l2  39278  cdleme21c  39284  cdleme21ct  39286  cdleme22aa  39296  cdleme22cN  39299  cdleme22d  39300  cdleme22e  39301  cdleme22eALTN  39302  cdleme23b  39307  cdleme25a  39310  cdleme25dN  39313  cdleme27N  39326  cdleme28a  39327  cdleme28b  39328  cdleme29ex  39331  cdleme32c  39400  cdleme42k  39441  cdlemg2cex  39548  cdlemg2idN  39553  cdlemg31c  39656  cdlemk5a  39792  cdlemk5  39793  congmul  41788  jm2.25lem1  41819  jm2.26  41823  jm2.27a  41826  infleinflem1  44159  stoweidlem42  44837