Theorem syl222anc 1413

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 1408	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  1500  3anandirs  1501  omopth2  8578  omeu  8579  dfac12lem2  10147  xaddass2  13294  xpncan  13295  divdenle  16833  pockthlem  16990  znidomb  21748  tanord1  26739  ang180lem5  27015  isosctrlem3  27022  log2tlbnd  27147  basellem1  27282  perfectlem2  27431  bposlem6  27490  dchrisum0flblem2  27710  pntpbnd1a  27786  mulsproplem1  28346  axcontlem8  29358  xlt2addrd  33141  s2f1  33300  xrge0addass  33367  xrge0npcan  33371  elrgspnlem1  33593  submatminr1  34231  carsgclctunlem2  34741  nmulss1  36727  nadddilem3  36735  4atexlemntlpq  40883  4atexlemnclw  40885  trlval2  40978  cdleme0moN  41040  cdleme16b  41094  cdleme16c  41095  cdleme16d  41096  cdleme16e  41097  cdleme17c  41103  cdlemeda  41113  cdleme20h  41131  cdleme20j  41133  cdleme20l2  41136  cdleme21c  41142  cdleme21ct  41144  cdleme22aa  41154  cdleme22cN  41157  cdleme22d  41158  cdleme22e  41159  cdleme22eALTN  41160  cdleme23b  41165  cdleme25a  41168  cdleme25dN  41171  cdleme27N  41184  cdleme28a  41185  cdleme28b  41186  cdleme29ex  41189  cdleme32c  41258  cdleme42k  41299  cdlemg2cex  41406  cdlemg2idN  41411  cdlemg31c  41514  cdlemk5a  41650  cdlemk5  41651  congmul  43735  jm2.25lem1  43766  jm2.26  43770  jm2.27a  43773  infleinflem1  46126  stoweidlem42  46797