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

This theorem is referenced by:  3anandis  1473  3anandirs  1474  omopth2  8551  omeu  8552  dfac12lem2  10105  xaddass2  13217  xpncan  13218  divdenle  16726  pockthlem  16883  znidomb  21478  tanord1  26453  ang180lem5  26730  isosctrlem3  26737  log2tlbnd  26862  basellem1  26998  perfectlem2  27148  bposlem6  27207  dchrisum0flblem2  27427  pntpbnd1a  27503  mulsproplem1  28026  axcontlem8  28905  xlt2addrd  32689  s2f1  32873  xrge0addass  32964  xrge0npcan  32968  elrgspnlem1  33200  submatminr1  33807  carsgclctunlem2  34317  4atexlemntlpq  40069  4atexlemnclw  40071  trlval2  40164  cdleme0moN  40226  cdleme16b  40280  cdleme16c  40281  cdleme16d  40282  cdleme16e  40283  cdleme17c  40289  cdlemeda  40299  cdleme20h  40317  cdleme20j  40319  cdleme20l2  40322  cdleme21c  40328  cdleme21ct  40330  cdleme22aa  40340  cdleme22cN  40343  cdleme22d  40344  cdleme22e  40345  cdleme22eALTN  40346  cdleme23b  40351  cdleme25a  40354  cdleme25dN  40357  cdleme27N  40370  cdleme28a  40371  cdleme28b  40372  cdleme29ex  40375  cdleme32c  40444  cdleme42k  40485  cdlemg2cex  40592  cdlemg2idN  40597  cdlemg31c  40700  cdlemk5a  40836  cdlemk5  40837  congmul  42963  jm2.25lem1  42994  jm2.26  42998  jm2.27a  43001  infleinflem1  45373  stoweidlem42  46047