Theorem syl222anc 1389

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 1384	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3anandis  1474  3anandirs  1475  omopth2  8519  omeu  8520  dfac12lem2  10067  xaddass2  13202  xpncan  13203  divdenle  16719  pockthlem  16876  znidomb  21541  tanord1  26501  ang180lem5  26777  isosctrlem3  26784  log2tlbnd  26909  basellem1  27044  perfectlem2  27193  bposlem6  27252  dchrisum0flblem2  27472  pntpbnd1a  27548  mulsproplem1  28108  axcontlem8  29040  xlt2addrd  32832  s2f1  33005  xrge0addass  33076  xrge0npcan  33080  elrgspnlem1  33303  submatminr1  33954  carsgclctunlem2  34463  4atexlemntlpq  40514  4atexlemnclw  40516  trlval2  40609  cdleme0moN  40671  cdleme16b  40725  cdleme16c  40726  cdleme16d  40727  cdleme16e  40728  cdleme17c  40734  cdlemeda  40744  cdleme20h  40762  cdleme20j  40764  cdleme20l2  40767  cdleme21c  40773  cdleme21ct  40775  cdleme22aa  40785  cdleme22cN  40788  cdleme22d  40789  cdleme22e  40790  cdleme22eALTN  40791  cdleme23b  40796  cdleme25a  40799  cdleme25dN  40802  cdleme27N  40815  cdleme28a  40816  cdleme28b  40817  cdleme29ex  40820  cdleme32c  40889  cdleme42k  40930  cdlemg2cex  41037  cdlemg2idN  41042  cdlemg31c  41145  cdlemk5a  41281  cdlemk5  41282  congmul  43395  jm2.25lem1  43426  jm2.26  43430  jm2.27a  43433  infleinflem1  45799  stoweidlem42  46470