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  8592  omeu  8593  dfac12lem2  10223  xaddass2  13380  xpncan  13381  divdenle  16925  pockthlem  17083  znidomb  21867  tanord1  26865  ang180lem5  27141  isosctrlem3  27148  log2tlbnd  27273  basellem1  27408  perfectlem2  27557  bposlem6  27616  dchrisum0flblem2  27836  pntpbnd1a  27912  mulsproplem1  28502  axcontlem8  29549  xlt2addrd  33351  s2f1  33510  xrge0addass  33577  xrge0npcan  33581  elrgspnlem1  33803  submatminr1  34442  carsgclctunlem2  34951  nmulss1  36963  nadddilem3  36971  4atexlemntlpq  41126  4atexlemnclw  41128  trlval2  41221  cdleme0moN  41283  cdleme16b  41337  cdleme16c  41338  cdleme16d  41339  cdleme16e  41340  cdleme17c  41346  cdlemeda  41356  cdleme20h  41374  cdleme20j  41376  cdleme20l2  41379  cdleme21c  41385  cdleme21ct  41387  cdleme22aa  41397  cdleme22cN  41400  cdleme22d  41401  cdleme22e  41402  cdleme22eALTN  41403  cdleme23b  41408  cdleme25a  41411  cdleme25dN  41414  cdleme27N  41427  cdleme28a  41428  cdleme28b  41429  cdleme29ex  41432  cdleme32c  41501  cdleme42k  41542  cdlemg2cex  41649  cdlemg2idN  41654  cdlemg31c  41757  cdlemk5a  41893  cdlemk5  41894  congmul  43974  jm2.25lem1  44005  jm2.26  44009  jm2.27a  44012  infleinflem1  46381  stoweidlem42  47052