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  8575  omeu  8576  dfac12lem2  10151  xaddass2  13306  xpncan  13307  divdenle  16846  pockthlem  17003  znidomb  21780  tanord1  26782  ang180lem5  27058  isosctrlem3  27065  log2tlbnd  27190  basellem1  27325  perfectlem2  27474  bposlem6  27533  dchrisum0flblem2  27753  pntpbnd1a  27829  mulsproplem1  28389  axcontlem8  29436  xlt2addrd  33238  s2f1  33397  xrge0addass  33464  xrge0npcan  33468  elrgspnlem1  33690  submatminr1  34328  carsgclctunlem2  34838  nmulss1  36802  nadddilem3  36810  4atexlemntlpq  40949  4atexlemnclw  40951  trlval2  41044  cdleme0moN  41106  cdleme16b  41160  cdleme16c  41161  cdleme16d  41162  cdleme16e  41163  cdleme17c  41169  cdlemeda  41179  cdleme20h  41197  cdleme20j  41199  cdleme20l2  41202  cdleme21c  41208  cdleme21ct  41210  cdleme22aa  41220  cdleme22cN  41223  cdleme22d  41224  cdleme22e  41225  cdleme22eALTN  41226  cdleme23b  41231  cdleme25a  41234  cdleme25dN  41237  cdleme27N  41250  cdleme28a  41251  cdleme28b  41252  cdleme29ex  41255  cdleme32c  41324  cdleme42k  41365  cdlemg2cex  41472  cdlemg2idN  41477  cdlemg31c  41580  cdlemk5a  41716  cdlemk5  41717  congmul  43816  jm2.25lem1  43847  jm2.26  43851  jm2.27a  43854  infleinflem1  46207  stoweidlem42  46878