Theorem syl222anc 1382

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 514	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁))
8		syl222anc.7	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)
9	1, 2, 3, 4, 7, 8	syl221anc 1377	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  3anandis  1467  3anandirs  1468  omopth2  8212  omeu  8213  dfac12lem2  9572  xaddass2  12646  xpncan  12647  divdenle  16091  pockthlem  16243  znidomb  20710  tanord1  25123  ang180lem5  25393  isosctrlem3  25400  log2tlbnd  25525  basellem1  25660  perfectlem2  25808  bposlem6  25867  dchrisum0flblem2  26087  pntpbnd1a  26163  axcontlem8  26759  xlt2addrd  30484  s2f1  30623  xrge0addass  30679  xrge0npcan  30683  submatminr1  31077  carsgclctunlem2  31579  4atexlemntlpq  37206  4atexlemnclw  37208  trlval2  37301  cdleme0moN  37363  cdleme16b  37417  cdleme16c  37418  cdleme16d  37419  cdleme16e  37420  cdleme17c  37426  cdlemeda  37436  cdleme20h  37454  cdleme20j  37456  cdleme20l2  37459  cdleme21c  37465  cdleme21ct  37467  cdleme22aa  37477  cdleme22cN  37480  cdleme22d  37481  cdleme22e  37482  cdleme22eALTN  37483  cdleme23b  37488  cdleme25a  37491  cdleme25dN  37494  cdleme27N  37507  cdleme28a  37508  cdleme28b  37509  cdleme29ex  37512  cdleme32c  37581  cdleme42k  37622  cdlemg2cex  37729  cdlemg2idN  37734  cdlemg31c  37837  cdlemk5a  37973  cdlemk5  37974  congmul  39571  jm2.25lem1  39602  jm2.26  39606  jm2.27a  39609  infleinflem1  41645  stoweidlem42  42334