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  8499  omeu  8500  dfac12lem2  10036  xaddass2  13149  xpncan  13150  divdenle  16660  pockthlem  16817  znidomb  21499  tanord1  26474  ang180lem5  26751  isosctrlem3  26758  log2tlbnd  26883  basellem1  27019  perfectlem2  27169  bposlem6  27228  dchrisum0flblem2  27448  pntpbnd1a  27524  mulsproplem1  28056  axcontlem8  28950  xlt2addrd  32740  s2f1  32924  xrge0addass  32995  xrge0npcan  32999  elrgspnlem1  33207  submatminr1  33821  carsgclctunlem2  34330  4atexlemntlpq  40113  4atexlemnclw  40115  trlval2  40208  cdleme0moN  40270  cdleme16b  40324  cdleme16c  40325  cdleme16d  40326  cdleme16e  40327  cdleme17c  40333  cdlemeda  40343  cdleme20h  40361  cdleme20j  40363  cdleme20l2  40366  cdleme21c  40372  cdleme21ct  40374  cdleme22aa  40384  cdleme22cN  40387  cdleme22d  40388  cdleme22e  40389  cdleme22eALTN  40390  cdleme23b  40395  cdleme25a  40398  cdleme25dN  40401  cdleme27N  40414  cdleme28a  40415  cdleme28b  40416  cdleme29ex  40419  cdleme32c  40488  cdleme42k  40529  cdlemg2cex  40636  cdlemg2idN  40641  cdlemg31c  40744  cdlemk5a  40880  cdlemk5  40881  congmul  43006  jm2.25lem1  43037  jm2.26  43041  jm2.27a  43044  infleinflem1  45414  stoweidlem42  46086