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  8509  omeu  8510  dfac12lem2  10058  xaddass2  13170  xpncan  13171  divdenle  16678  pockthlem  16835  znidomb  21486  tanord1  26462  ang180lem5  26739  isosctrlem3  26746  log2tlbnd  26871  basellem1  27007  perfectlem2  27157  bposlem6  27216  dchrisum0flblem2  27436  pntpbnd1a  27512  mulsproplem1  28042  axcontlem8  28934  xlt2addrd  32715  s2f1  32899  xrge0addass  32983  xrge0npcan  32987  elrgspnlem1  33195  submatminr1  33779  carsgclctunlem2  34289  4atexlemntlpq  40050  4atexlemnclw  40052  trlval2  40145  cdleme0moN  40207  cdleme16b  40261  cdleme16c  40262  cdleme16d  40263  cdleme16e  40264  cdleme17c  40270  cdlemeda  40280  cdleme20h  40298  cdleme20j  40300  cdleme20l2  40303  cdleme21c  40309  cdleme21ct  40311  cdleme22aa  40321  cdleme22cN  40324  cdleme22d  40325  cdleme22e  40326  cdleme22eALTN  40327  cdleme23b  40332  cdleme25a  40335  cdleme25dN  40338  cdleme27N  40351  cdleme28a  40352  cdleme28b  40353  cdleme29ex  40356  cdleme32c  40425  cdleme42k  40466  cdlemg2cex  40573  cdlemg2idN  40578  cdlemg31c  40681  cdlemk5a  40817  cdlemk5  40818  congmul  42943  jm2.25lem1  42974  jm2.26  42978  jm2.27a  42981  infleinflem1  45353  stoweidlem42  46027