Theorem syl222anc 1394

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3anandis  1479  3anandirs  1480  omopth2  8516  omeu  8517  dfac12lem2  10065  xaddass2  13200  xpncan  13201  divdenle  16717  pockthlem  16874  znidomb  21543  tanord1  26526  ang180lem5  26802  isosctrlem3  26809  log2tlbnd  26934  basellem1  27069  perfectlem2  27218  bposlem6  27277  dchrisum0flblem2  27497  pntpbnd1a  27573  mulsproplem1  28133  axcontlem8  29065  xlt2addrd  32858  s2f1  33031  xrge0addass  33102  xrge0npcan  33106  elrgspnlem1  33330  submatminr1  34001  carsgclctunlem2  34510  4atexlemntlpq  40567  4atexlemnclw  40569  trlval2  40662  cdleme0moN  40724  cdleme16b  40778  cdleme16c  40779  cdleme16d  40780  cdleme16e  40781  cdleme17c  40787  cdlemeda  40797  cdleme20h  40815  cdleme20j  40817  cdleme20l2  40820  cdleme21c  40826  cdleme21ct  40828  cdleme22aa  40838  cdleme22cN  40841  cdleme22d  40842  cdleme22e  40843  cdleme22eALTN  40844  cdleme23b  40849  cdleme25a  40852  cdleme25dN  40855  cdleme27N  40868  cdleme28a  40869  cdleme28b  40870  cdleme29ex  40873  cdleme32c  40942  cdleme42k  40983  cdlemg2cex  41090  cdlemg2idN  41095  cdlemg31c  41198  cdlemk5a  41334  cdlemk5  41335  congmul  43419  jm2.25lem1  43450  jm2.26  43454  jm2.27a  43457  infleinflem1  45821  stoweidlem42  46492