Theorem syl222anc 1389

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 1384	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  1474  3anandirs  1475  omopth2  8521  omeu  8522  dfac12lem2  10067  xaddass2  13177  xpncan  13178  divdenle  16688  pockthlem  16845  znidomb  21528  tanord1  26514  ang180lem5  26791  isosctrlem3  26798  log2tlbnd  26923  basellem1  27059  perfectlem2  27209  bposlem6  27268  dchrisum0flblem2  27488  pntpbnd1a  27564  mulsproplem1  28124  axcontlem8  29056  xlt2addrd  32849  s2f1  33037  xrge0addass  33108  xrge0npcan  33112  elrgspnlem1  33335  submatminr1  33987  carsgclctunlem2  34496  4atexlemntlpq  40441  4atexlemnclw  40443  trlval2  40536  cdleme0moN  40598  cdleme16b  40652  cdleme16c  40653  cdleme16d  40654  cdleme16e  40655  cdleme17c  40661  cdlemeda  40671  cdleme20h  40689  cdleme20j  40691  cdleme20l2  40694  cdleme21c  40700  cdleme21ct  40702  cdleme22aa  40712  cdleme22cN  40715  cdleme22d  40716  cdleme22e  40717  cdleme22eALTN  40718  cdleme23b  40723  cdleme25a  40726  cdleme25dN  40729  cdleme27N  40742  cdleme28a  40743  cdleme28b  40744  cdleme29ex  40747  cdleme32c  40816  cdleme42k  40857  cdlemg2cex  40964  cdlemg2idN  40969  cdlemg31c  41072  cdlemk5a  41208  cdlemk5  41209  congmul  43321  jm2.25lem1  43352  jm2.26  43356  jm2.27a  43359  infleinflem1  45725  stoweidlem42  46397