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  8507  omeu  8508  dfac12lem2  10045  xaddass2  13153  xpncan  13154  divdenle  16664  pockthlem  16821  znidomb  21502  tanord1  26476  ang180lem5  26753  isosctrlem3  26760  log2tlbnd  26885  basellem1  27021  perfectlem2  27171  bposlem6  27230  dchrisum0flblem2  27450  pntpbnd1a  27526  mulsproplem1  28058  axcontlem8  28953  xlt2addrd  32748  s2f1  32935  xrge0addass  33006  xrge0npcan  33010  elrgspnlem1  33218  submatminr1  33846  carsgclctunlem2  34355  4atexlemntlpq  40190  4atexlemnclw  40192  trlval2  40285  cdleme0moN  40347  cdleme16b  40401  cdleme16c  40402  cdleme16d  40403  cdleme16e  40404  cdleme17c  40410  cdlemeda  40420  cdleme20h  40438  cdleme20j  40440  cdleme20l2  40443  cdleme21c  40449  cdleme21ct  40451  cdleme22aa  40461  cdleme22cN  40464  cdleme22d  40465  cdleme22e  40466  cdleme22eALTN  40467  cdleme23b  40472  cdleme25a  40475  cdleme25dN  40478  cdleme27N  40491  cdleme28a  40492  cdleme28b  40493  cdleme29ex  40496  cdleme32c  40565  cdleme42k  40606  cdlemg2cex  40713  cdlemg2idN  40718  cdlemg31c  40821  cdlemk5a  40957  cdlemk5  40958  congmul  43087  jm2.25lem1  43118  jm2.26  43122  jm2.27a  43125  infleinflem1  45495  stoweidlem42  46167