Theorem syl222anc 1333

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1030

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 195  df-an 384  df-3an 1032

This theorem is referenced by:  3anandis  1425  3anandirs  1426  omopth2  7524  omeu  7525  dfac12lem2  8822  xaddass2  11905  xpncan  11906  divdenle  15237  pockthlem  15389  znidomb  19670  tanord1  24000  ang180lem5  24256  isosctrlem3  24263  log2tlbnd  24385  basellem1  24520  perfectlem2  24668  bposlem6  24727  dchrisum0flblem2  24911  pntpbnd1a  24987  axcontlem8  25565  xlt2addrd  28715  xrge0addass  28823  xrge0npcan  28827  submatminr1  29006  carsgclctunlem2  29510  4atexlemntlpq  34171  4atexlemnclw  34173  trlval2  34267  cdleme0moN  34329  cdleme16b  34383  cdleme16c  34384  cdleme16d  34385  cdleme16e  34386  cdleme17c  34392  cdlemeda  34402  cdleme20h  34421  cdleme20j  34423  cdleme20l2  34426  cdleme21c  34432  cdleme21ct  34434  cdleme22aa  34444  cdleme22cN  34447  cdleme22d  34448  cdleme22e  34449  cdleme22eALTN  34450  cdleme23b  34455  cdleme25a  34458  cdleme25dN  34461  cdleme27N  34474  cdleme28a  34475  cdleme28b  34476  cdleme29ex  34479  cdleme32c  34548  cdleme42k  34589  cdlemg2cex  34696  cdlemg2idN  34701  cdlemg31c  34804  cdlemk5a  34940  cdlemk5  34941  congmul  36351  jm2.25lem1  36382  jm2.26  36386  jm2.27a  36389  infleinflem1  38327  stoweidlem42  38735