Theorem syl222anc 1386

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3anandis  1471  3anandirs  1472  omopth2  8580  omeu  8581  dfac12lem2  10135  xaddass2  13225  xpncan  13226  divdenle  16681  pockthlem  16834  znidomb  21108  tanord1  26037  ang180lem5  26307  isosctrlem3  26314  log2tlbnd  26439  basellem1  26574  perfectlem2  26722  bposlem6  26781  dchrisum0flblem2  27001  pntpbnd1a  27077  mulsproplem1  27561  axcontlem8  28218  xlt2addrd  31958  s2f1  32098  xrge0addass  32178  xrge0npcan  32182  submatminr1  32778  carsgclctunlem2  33306  4atexlemntlpq  38927  4atexlemnclw  38929  trlval2  39022  cdleme0moN  39084  cdleme16b  39138  cdleme16c  39139  cdleme16d  39140  cdleme16e  39141  cdleme17c  39147  cdlemeda  39157  cdleme20h  39175  cdleme20j  39177  cdleme20l2  39180  cdleme21c  39186  cdleme21ct  39188  cdleme22aa  39198  cdleme22cN  39201  cdleme22d  39202  cdleme22e  39203  cdleme22eALTN  39204  cdleme23b  39209  cdleme25a  39212  cdleme25dN  39215  cdleme27N  39228  cdleme28a  39229  cdleme28b  39230  cdleme29ex  39233  cdleme32c  39302  cdleme42k  39343  cdlemg2cex  39450  cdlemg2idN  39455  cdlemg31c  39558  cdlemk5a  39694  cdlemk5  39695  congmul  41691  jm2.25lem1  41722  jm2.26  41726  jm2.27a  41729  infleinflem1  44066  stoweidlem42  44744