Theorem syl222anc 1414

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anandis  1501  3anandirs  1502  omopth2  8623  omeu  8624  dfac12lem2  10253  xaddass2  13410  xpncan  13411  divdenle  16957  pockthlem  17115  znidomb  21900  tanord1  26898  ang180lem5  27174  isosctrlem3  27181  log2tlbnd  27306  basellem1  27441  perfectlem2  27590  bposlem6  27649  dchrisum0flblem2  27869  pntpbnd1a  27945  mulsproplem1  28535  axcontlem8  29582  xlt2addrd  33424  s2f1  33583  xrge0addass  33653  xrge0npcan  33657  elrgspnlem1  33879  submatminr1  34525  carsgclctunlem2  35034  nmulss1  37154  nadddilem3  37162  4atexlemntlpq  41328  4atexlemnclw  41330  trlval2  41423  cdleme0moN  41485  cdleme16b  41539  cdleme16c  41540  cdleme16d  41541  cdleme16e  41542  cdleme17c  41548  cdlemeda  41558  cdleme20h  41576  cdleme20j  41578  cdleme20l2  41581  cdleme21c  41587  cdleme21ct  41589  cdleme22aa  41599  cdleme22cN  41602  cdleme22d  41603  cdleme22e  41604  cdleme22eALTN  41605  cdleme23b  41610  cdleme25a  41613  cdleme25dN  41616  cdleme27N  41629  cdleme28a  41630  cdleme28b  41631  cdleme29ex  41634  cdleme32c  41703  cdleme42k  41744  cdlemg2cex  41851  cdlemg2idN  41856  cdlemg31c  41959  cdlemk5a  42095  cdlemk5  42096  congmul  44178  jm2.25lem1  44209  jm2.26  44213  jm2.27a  44216  infleinflem1  46596  stoweidlem42  47267