Theorem syl222anc 1409

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3anandis  1495  3anandirs  1496  omopth2  8557  omeu  8558  dfac12lem2  10116  xaddass2  13264  xpncan  13265  divdenle  16796  pockthlem  16953  znidomb  21668  tanord1  26656  ang180lem5  26932  isosctrlem3  26939  log2tlbnd  27064  basellem1  27199  perfectlem2  27348  bposlem6  27407  dchrisum0flblem2  27627  pntpbnd1a  27703  mulsproplem1  28263  axcontlem8  29226  xlt2addrd  33012  s2f1  33173  xrge0addass  33244  xrge0npcan  33248  elrgspnlem1  33470  submatminr1  34112  carsgclctunlem2  34621  4atexlemntlpq  40699  4atexlemnclw  40701  trlval2  40794  cdleme0moN  40856  cdleme16b  40910  cdleme16c  40911  cdleme16d  40912  cdleme16e  40913  cdleme17c  40919  cdlemeda  40929  cdleme20h  40947  cdleme20j  40949  cdleme20l2  40952  cdleme21c  40958  cdleme21ct  40960  cdleme22aa  40970  cdleme22cN  40973  cdleme22d  40974  cdleme22e  40975  cdleme22eALTN  40976  cdleme23b  40981  cdleme25a  40984  cdleme25dN  40987  cdleme27N  41000  cdleme28a  41001  cdleme28b  41002  cdleme29ex  41005  cdleme32c  41074  cdleme42k  41115  cdlemg2cex  41222  cdlemg2idN  41227  cdlemg31c  41330  cdlemk5a  41466  cdlemk5  41467  congmul  43551  jm2.25lem1  43582  jm2.26  43586  jm2.27a  43589  infleinflem1  45944  stoweidlem42  46615