Theorem syl222anc 1493

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl33anc.6	⊢ (𝜑 → 𝜁)
syl222anc.7	⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)

Assertion

Ref	Expression
syl222anc	⊢ (𝜑 → 𝜎)

Proof of Theorem syl222anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6		syl33anc.6	. . 3 ⊢ (𝜑 → 𝜁)
7	5, 6	jca 555	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁))
8		syl222anc.7	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)
9	1, 2, 3, 4, 7, 8	syl221anc 1488	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  3anandis  1583  3anandirs  1584  omopth2  7835  omeu  7836  dfac12lem2  9178  xaddass2  12293  xpncan  12294  divdenle  15679  pockthlem  15831  znidomb  20132  tanord1  24503  ang180lem5  24763  isosctrlem3  24770  log2tlbnd  24892  basellem1  25027  perfectlem2  25175  bposlem6  25234  dchrisum0flblem2  25418  pntpbnd1a  25494  axcontlem8  26071  xlt2addrd  29853  xrge0addass  30020  xrge0npcan  30024  submatminr1  30206  carsgclctunlem2  30711  4atexlemntlpq  35875  4atexlemnclw  35877  trlval2  35971  cdleme0moN  36033  cdleme16b  36087  cdleme16c  36088  cdleme16d  36089  cdleme16e  36090  cdleme17c  36096  cdlemeda  36106  cdleme20h  36124  cdleme20j  36126  cdleme20l2  36129  cdleme21c  36135  cdleme21ct  36137  cdleme22aa  36147  cdleme22cN  36150  cdleme22d  36151  cdleme22e  36152  cdleme22eALTN  36153  cdleme23b  36158  cdleme25a  36161  cdleme25dN  36164  cdleme27N  36177  cdleme28a  36178  cdleme28b  36179  cdleme29ex  36182  cdleme32c  36251  cdleme42k  36292  cdlemg2cex  36399  cdlemg2idN  36404  cdlemg31c  36507  cdlemk5a  36643  cdlemk5  36644  congmul  38054  jm2.25lem1  38085  jm2.26  38089  jm2.27a  38092  infleinflem1  40102  stoweidlem42  40780