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  8511  omeu  8512  dfac12lem2  10055  xaddass2  13165  xpncan  13166  divdenle  16676  pockthlem  16833  znidomb  21516  tanord1  26502  ang180lem5  26779  isosctrlem3  26786  log2tlbnd  26911  basellem1  27047  perfectlem2  27197  bposlem6  27256  dchrisum0flblem2  27476  pntpbnd1a  27552  mulsproplem1  28112  axcontlem8  29044  xlt2addrd  32839  s2f1  33027  xrge0addass  33098  xrge0npcan  33102  elrgspnlem1  33324  submatminr1  33967  carsgclctunlem2  34476  4atexlemntlpq  40328  4atexlemnclw  40330  trlval2  40423  cdleme0moN  40485  cdleme16b  40539  cdleme16c  40540  cdleme16d  40541  cdleme16e  40542  cdleme17c  40548  cdlemeda  40558  cdleme20h  40576  cdleme20j  40578  cdleme20l2  40581  cdleme21c  40587  cdleme21ct  40589  cdleme22aa  40599  cdleme22cN  40602  cdleme22d  40603  cdleme22e  40604  cdleme22eALTN  40605  cdleme23b  40610  cdleme25a  40613  cdleme25dN  40616  cdleme27N  40629  cdleme28a  40630  cdleme28b  40631  cdleme29ex  40634  cdleme32c  40703  cdleme42k  40744  cdlemg2cex  40851  cdlemg2idN  40856  cdlemg31c  40959  cdlemk5a  41095  cdlemk5  41096  congmul  43209  jm2.25lem1  43240  jm2.26  43244  jm2.27a  43247  infleinflem1  45614  stoweidlem42  46286