Theorem syl222anc 1454

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  3anandis  1544  3anandirs  1545  omopth2  7948  omeu  7949  dfac12lem2  9301  xaddass2  12392  xpncan  12393  divdenle  15861  pockthlem  16013  znidomb  20305  tanord1  24721  ang180lem5  24991  isosctrlem3  24998  log2tlbnd  25124  basellem1  25259  perfectlem2  25407  bposlem6  25466  dchrisum0flblem2  25650  pntpbnd1a  25726  axcontlem8  26320  xlt2addrd  30088  xrge0addass  30252  xrge0npcan  30256  submatminr1  30474  carsgclctunlem2  30979  4atexlemntlpq  36206  4atexlemnclw  36208  trlval2  36301  cdleme0moN  36363  cdleme16b  36417  cdleme16c  36418  cdleme16d  36419  cdleme16e  36420  cdleme17c  36426  cdlemeda  36436  cdleme20h  36454  cdleme20j  36456  cdleme20l2  36459  cdleme21c  36465  cdleme21ct  36467  cdleme22aa  36477  cdleme22cN  36480  cdleme22d  36481  cdleme22e  36482  cdleme22eALTN  36483  cdleme23b  36488  cdleme25a  36491  cdleme25dN  36494  cdleme27N  36507  cdleme28a  36508  cdleme28b  36509  cdleme29ex  36512  cdleme32c  36581  cdleme42k  36622  cdlemg2cex  36729  cdlemg2idN  36734  cdlemg31c  36837  cdlemk5a  36973  cdlemk5  36974  congmul  38475  jm2.25lem1  38506  jm2.26  38510  jm2.27a  38513  infleinflem1  40476  stoweidlem42  41168