Theorem syl222anc 1385

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

This theorem is referenced by:  3anandis  1470  3anandirs  1471  omopth2  8588  omeu  8589  dfac12lem2  10143  xaddass2  13234  xpncan  13235  divdenle  16690  pockthlem  16843  znidomb  21337  tanord1  26283  ang180lem5  26555  isosctrlem3  26562  log2tlbnd  26687  basellem1  26822  perfectlem2  26970  bposlem6  27029  dchrisum0flblem2  27249  pntpbnd1a  27325  mulsproplem1  27812  axcontlem8  28497  xlt2addrd  32239  s2f1  32379  xrge0addass  32459  xrge0npcan  32463  submatminr1  33089  carsgclctunlem2  33617  4atexlemntlpq  39243  4atexlemnclw  39245  trlval2  39338  cdleme0moN  39400  cdleme16b  39454  cdleme16c  39455  cdleme16d  39456  cdleme16e  39457  cdleme17c  39463  cdlemeda  39473  cdleme20h  39491  cdleme20j  39493  cdleme20l2  39496  cdleme21c  39502  cdleme21ct  39504  cdleme22aa  39514  cdleme22cN  39517  cdleme22d  39518  cdleme22e  39519  cdleme22eALTN  39520  cdleme23b  39525  cdleme25a  39528  cdleme25dN  39531  cdleme27N  39544  cdleme28a  39545  cdleme28b  39546  cdleme29ex  39549  cdleme32c  39618  cdleme42k  39659  cdlemg2cex  39766  cdlemg2idN  39771  cdlemg31c  39874  cdlemk5a  40010  cdlemk5  40011  congmul  42009  jm2.25lem1  42040  jm2.26  42044  jm2.27a  42047  infleinflem1  44379  stoweidlem42  45057