Theorem syl222anc 1389

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3anandis  1474  3anandirs  1475  omopth2  8512  omeu  8513  dfac12lem2  10058  xaddass2  13193  xpncan  13194  divdenle  16710  pockthlem  16867  znidomb  21551  tanord1  26514  ang180lem5  26790  isosctrlem3  26797  log2tlbnd  26922  basellem1  27058  perfectlem2  27207  bposlem6  27266  dchrisum0flblem2  27486  pntpbnd1a  27562  mulsproplem1  28122  axcontlem8  29054  xlt2addrd  32847  s2f1  33020  xrge0addass  33091  xrge0npcan  33095  elrgspnlem1  33318  submatminr1  33970  carsgclctunlem2  34479  4atexlemntlpq  40528  4atexlemnclw  40530  trlval2  40623  cdleme0moN  40685  cdleme16b  40739  cdleme16c  40740  cdleme16d  40741  cdleme16e  40742  cdleme17c  40748  cdlemeda  40758  cdleme20h  40776  cdleme20j  40778  cdleme20l2  40781  cdleme21c  40787  cdleme21ct  40789  cdleme22aa  40799  cdleme22cN  40802  cdleme22d  40803  cdleme22e  40804  cdleme22eALTN  40805  cdleme23b  40810  cdleme25a  40813  cdleme25dN  40816  cdleme27N  40829  cdleme28a  40830  cdleme28b  40831  cdleme29ex  40834  cdleme32c  40903  cdleme42k  40944  cdlemg2cex  41051  cdlemg2idN  41056  cdlemg31c  41159  cdlemk5a  41295  cdlemk5  41296  congmul  43413  jm2.25lem1  43444  jm2.26  43448  jm2.27a  43451  infleinflem1  45817  stoweidlem42  46488