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  8576  omeu  8577  dfac12lem2  10204  xaddass2  13361  xpncan  13362  divdenle  16905  pockthlem  17063  znidomb  21847  tanord1  26847  ang180lem5  27123  isosctrlem3  27130  log2tlbnd  27255  basellem1  27390  perfectlem2  27539  bposlem6  27598  dchrisum0flblem2  27818  pntpbnd1a  27894  mulsproplem1  28484  axcontlem8  29531  xlt2addrd  33333  s2f1  33492  xrge0addass  33559  xrge0npcan  33563  elrgspnlem1  33785  submatminr1  34424  carsgclctunlem2  34934  nmulss1  36933  nadddilem3  36941  4atexlemntlpq  41093  4atexlemnclw  41095  trlval2  41188  cdleme0moN  41250  cdleme16b  41304  cdleme16c  41305  cdleme16d  41306  cdleme16e  41307  cdleme17c  41313  cdlemeda  41323  cdleme20h  41341  cdleme20j  41343  cdleme20l2  41346  cdleme21c  41352  cdleme21ct  41354  cdleme22aa  41364  cdleme22cN  41367  cdleme22d  41368  cdleme22e  41369  cdleme22eALTN  41370  cdleme23b  41375  cdleme25a  41378  cdleme25dN  41381  cdleme27N  41394  cdleme28a  41395  cdleme28b  41396  cdleme29ex  41399  cdleme32c  41468  cdleme42k  41509  cdlemg2cex  41616  cdlemg2idN  41621  cdlemg31c  41724  cdlemk5a  41860  cdlemk5  41861  congmul  43927  jm2.25lem1  43958  jm2.26  43962  jm2.27a  43965  infleinflem1  46325  stoweidlem42  46996