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  8590  omeu  8591  dfac12lem2  10145  xaddass2  13236  xpncan  13237  divdenle  16692  pockthlem  16845  znidomb  21340  tanord1  26297  ang180lem5  26569  isosctrlem3  26576  log2tlbnd  26701  basellem1  26836  perfectlem2  26984  bposlem6  27043  dchrisum0flblem2  27263  pntpbnd1a  27339  mulsproplem1  27826  axcontlem8  28511  xlt2addrd  32253  s2f1  32393  xrge0addass  32473  xrge0npcan  32477  submatminr1  33103  carsgclctunlem2  33631  4atexlemntlpq  39255  4atexlemnclw  39257  trlval2  39350  cdleme0moN  39412  cdleme16b  39466  cdleme16c  39467  cdleme16d  39468  cdleme16e  39469  cdleme17c  39475  cdlemeda  39485  cdleme20h  39503  cdleme20j  39505  cdleme20l2  39508  cdleme21c  39514  cdleme21ct  39516  cdleme22aa  39526  cdleme22cN  39529  cdleme22d  39530  cdleme22e  39531  cdleme22eALTN  39532  cdleme23b  39537  cdleme25a  39540  cdleme25dN  39543  cdleme27N  39556  cdleme28a  39557  cdleme28b  39558  cdleme29ex  39561  cdleme32c  39630  cdleme42k  39671  cdlemg2cex  39778  cdlemg2idN  39783  cdlemg31c  39886  cdlemk5a  40022  cdlemk5  40023  congmul  42021  jm2.25lem1  42052  jm2.26  42056  jm2.27a  42059  infleinflem1  44391  stoweidlem42  45069