Theorem syl222anc 1382

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)

Hypotheses

Ref	Expression
syl12anc.1	⊢ (𝜑 → 𝜓)
syl12anc.2	⊢ (𝜑 → 𝜒)
syl12anc.3	⊢ (𝜑 → 𝜃)
syl22anc.4	⊢ (𝜑 → 𝜏)
syl23anc.5	⊢ (𝜑 → 𝜂)
syl33anc.6	⊢ (𝜑 → 𝜁)
syl222anc.7	⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)

Assertion

Ref	Expression
syl222anc	⊢ (𝜑 → 𝜎)

Proof of Theorem syl222anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl12anc.2	. 2 ⊢ (𝜑 → 𝜒)
3		syl12anc.3	. 2 ⊢ (𝜑 → 𝜃)
4		syl22anc.4	. 2 ⊢ (𝜑 → 𝜏)
5		syl23anc.5	. . 3 ⊢ (𝜑 → 𝜂)
6		syl33anc.6	. . 3 ⊢ (𝜑 → 𝜁)
7	5, 6	jca 553	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁))
8		syl222anc.7	. 2 ⊢ (((𝜓 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁)) → 𝜎)
9	1, 2, 3, 4, 7, 8	syl221anc 1377	1 ⊢ (𝜑 → 𝜎)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1054

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  3anandis  1474  3anandirs  1475  omopth2  7709  omeu  7710  dfac12lem2  9004  xaddass2  12118  xpncan  12119  divdenle  15504  pockthlem  15656  znidomb  19958  tanord1  24328  ang180lem5  24588  isosctrlem3  24595  log2tlbnd  24717  basellem1  24852  perfectlem2  25000  bposlem6  25059  dchrisum0flblem2  25243  pntpbnd1a  25319  axcontlem8  25896  xlt2addrd  29651  xrge0addass  29818  xrge0npcan  29822  submatminr1  30004  carsgclctunlem2  30509  4atexlemntlpq  35672  4atexlemnclw  35674  trlval2  35768  cdleme0moN  35830  cdleme16b  35884  cdleme16c  35885  cdleme16d  35886  cdleme16e  35887  cdleme17c  35893  cdlemeda  35903  cdleme20h  35921  cdleme20j  35923  cdleme20l2  35926  cdleme21c  35932  cdleme21ct  35934  cdleme22aa  35944  cdleme22cN  35947  cdleme22d  35948  cdleme22e  35949  cdleme22eALTN  35950  cdleme23b  35955  cdleme25a  35958  cdleme25dN  35961  cdleme27N  35974  cdleme28a  35975  cdleme28b  35976  cdleme29ex  35979  cdleme32c  36048  cdleme42k  36089  cdlemg2cex  36196  cdlemg2idN  36201  cdlemg31c  36304  cdlemk5a  36440  cdlemk5  36441  congmul  37851  jm2.25lem1  37882  jm2.26  37886  jm2.27a  37889  infleinflem1  39899  stoweidlem42  40577