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 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  1473  3anandirs  1474  omopth2  8622  omeu  8623  dfac12lem2  10185  xaddass2  13292  xpncan  13293  divdenle  16786  pockthlem  16943  znidomb  21580  tanord1  26579  ang180lem5  26856  isosctrlem3  26863  log2tlbnd  26988  basellem1  27124  perfectlem2  27274  bposlem6  27333  dchrisum0flblem2  27553  pntpbnd1a  27629  mulsproplem1  28142  axcontlem8  28986  xlt2addrd  32762  s2f1  32929  xrge0addass  33021  xrge0npcan  33025  elrgspnlem1  33246  submatminr1  33809  carsgclctunlem2  34321  4atexlemntlpq  40070  4atexlemnclw  40072  trlval2  40165  cdleme0moN  40227  cdleme16b  40281  cdleme16c  40282  cdleme16d  40283  cdleme16e  40284  cdleme17c  40290  cdlemeda  40300  cdleme20h  40318  cdleme20j  40320  cdleme20l2  40323  cdleme21c  40329  cdleme21ct  40331  cdleme22aa  40341  cdleme22cN  40344  cdleme22d  40345  cdleme22e  40346  cdleme22eALTN  40347  cdleme23b  40352  cdleme25a  40355  cdleme25dN  40358  cdleme27N  40371  cdleme28a  40372  cdleme28b  40373  cdleme29ex  40376  cdleme32c  40445  cdleme42k  40486  cdlemg2cex  40593  cdlemg2idN  40598  cdlemg31c  40701  cdlemk5a  40837  cdlemk5  40838  congmul  42979  jm2.25lem1  43010  jm2.26  43014  jm2.27a  43017  infleinflem1  45381  stoweidlem42  46057