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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3anandis  1471  3anandirs  1472  omopth2  8640  omeu  8641  dfac12lem2  10214  xaddass2  13312  xpncan  13313  divdenle  16796  pockthlem  16952  znidomb  21603  tanord1  26597  ang180lem5  26874  isosctrlem3  26881  log2tlbnd  27006  basellem1  27142  perfectlem2  27292  bposlem6  27351  dchrisum0flblem2  27571  pntpbnd1a  27647  mulsproplem1  28160  axcontlem8  29004  xlt2addrd  32765  s2f1  32911  xrge0addass  33002  xrge0npcan  33006  submatminr1  33756  carsgclctunlem2  34284  4atexlemntlpq  40025  4atexlemnclw  40027  trlval2  40120  cdleme0moN  40182  cdleme16b  40236  cdleme16c  40237  cdleme16d  40238  cdleme16e  40239  cdleme17c  40245  cdlemeda  40255  cdleme20h  40273  cdleme20j  40275  cdleme20l2  40278  cdleme21c  40284  cdleme21ct  40286  cdleme22aa  40296  cdleme22cN  40299  cdleme22d  40300  cdleme22e  40301  cdleme22eALTN  40302  cdleme23b  40307  cdleme25a  40310  cdleme25dN  40313  cdleme27N  40326  cdleme28a  40327  cdleme28b  40328  cdleme29ex  40331  cdleme32c  40400  cdleme42k  40441  cdlemg2cex  40548  cdlemg2idN  40553  cdlemg31c  40656  cdlemk5a  40792  cdlemk5  40793  congmul  42924  jm2.25lem1  42955  jm2.26  42959  jm2.27a  42962  infleinflem1  45285  stoweidlem42  45963