Theorem syl222anc 1381

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

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

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 1084

This theorem is referenced by:  3anandis  1465  3anandirs  1466  omopth2  8202  omeu  8203  dfac12lem2  9562  xaddass2  12635  xpncan  12636  divdenle  16081  pockthlem  16233  znidomb  20700  tanord1  25113  ang180lem5  25383  isosctrlem3  25390  log2tlbnd  25515  basellem1  25650  perfectlem2  25798  bposlem6  25857  dchrisum0flblem2  26077  pntpbnd1a  26153  axcontlem8  26749  xlt2addrd  30474  s2f1  30614  xrge0addass  30670  xrge0npcan  30674  submatminr1  31068  carsgclctunlem2  31570  4atexlemntlpq  37196  4atexlemnclw  37198  trlval2  37291  cdleme0moN  37353  cdleme16b  37407  cdleme16c  37408  cdleme16d  37409  cdleme16e  37410  cdleme17c  37416  cdlemeda  37426  cdleme20h  37444  cdleme20j  37446  cdleme20l2  37449  cdleme21c  37455  cdleme21ct  37457  cdleme22aa  37467  cdleme22cN  37470  cdleme22d  37471  cdleme22e  37472  cdleme22eALTN  37473  cdleme23b  37478  cdleme25a  37481  cdleme25dN  37484  cdleme27N  37497  cdleme28a  37498  cdleme28b  37499  cdleme29ex  37502  cdleme32c  37571  cdleme42k  37612  cdlemg2cex  37719  cdlemg2idN  37724  cdlemg31c  37827  cdlemk5a  37963  cdlemk5  37964  congmul  39554  jm2.25lem1  39585  jm2.26  39589  jm2.27a  39592  infleinflem1  41627  stoweidlem42  42317