Theorem syl222anc 1386

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ 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 206  df-an 398  df-3an 1089

This theorem is referenced by:  3anandis  1471  3anandirs  1472  omopth2  8446  omeu  8447  dfac12lem2  9946  xaddass2  13030  xpncan  13031  divdenle  16498  pockthlem  16651  znidomb  20814  tanord1  25738  ang180lem5  26008  isosctrlem3  26015  log2tlbnd  26140  basellem1  26275  perfectlem2  26423  bposlem6  26482  dchrisum0flblem2  26702  pntpbnd1a  26778  axcontlem8  27384  xlt2addrd  31126  s2f1  31264  xrge0addass  31344  xrge0npcan  31348  submatminr1  31805  carsgclctunlem2  32331  4atexlemntlpq  38124  4atexlemnclw  38126  trlval2  38219  cdleme0moN  38281  cdleme16b  38335  cdleme16c  38336  cdleme16d  38337  cdleme16e  38338  cdleme17c  38344  cdlemeda  38354  cdleme20h  38372  cdleme20j  38374  cdleme20l2  38377  cdleme21c  38383  cdleme21ct  38385  cdleme22aa  38395  cdleme22cN  38398  cdleme22d  38399  cdleme22e  38400  cdleme22eALTN  38401  cdleme23b  38406  cdleme25a  38409  cdleme25dN  38412  cdleme27N  38425  cdleme28a  38426  cdleme28b  38427  cdleme29ex  38430  cdleme32c  38499  cdleme42k  38540  cdlemg2cex  38647  cdlemg2idN  38652  cdlemg31c  38755  cdlemk5a  38891  cdlemk5  38892  congmul  40827  jm2.25lem1  40858  jm2.26  40862  jm2.27a  40865  infleinflem1  42957  stoweidlem42  43632