Theorem syl222anc 1334

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 1329	1 ⊢ (𝜑 → 𝜎)

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

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  3anandis  1426  3anandirs  1427  omopth2  7551  omeu  7552  dfac12lem2  8849  xaddass2  11952  xpncan  11953  divdenle  15295  pockthlem  15447  znidomb  19729  tanord1  24087  ang180lem5  24343  isosctrlem3  24350  log2tlbnd  24472  basellem1  24607  perfectlem2  24755  bposlem6  24814  dchrisum0flblem2  24998  pntpbnd1a  25074  axcontlem8  25651  xlt2addrd  28913  xrge0addass  29021  xrge0npcan  29025  submatminr1  29204  carsgclctunlem2  29708  4atexlemntlpq  34372  4atexlemnclw  34374  trlval2  34468  cdleme0moN  34530  cdleme16b  34584  cdleme16c  34585  cdleme16d  34586  cdleme16e  34587  cdleme17c  34593  cdlemeda  34603  cdleme20h  34622  cdleme20j  34624  cdleme20l2  34627  cdleme21c  34633  cdleme21ct  34635  cdleme22aa  34645  cdleme22cN  34648  cdleme22d  34649  cdleme22e  34650  cdleme22eALTN  34651  cdleme23b  34656  cdleme25a  34659  cdleme25dN  34662  cdleme27N  34675  cdleme28a  34676  cdleme28b  34677  cdleme29ex  34680  cdleme32c  34749  cdleme42k  34790  cdlemg2cex  34897  cdlemg2idN  34902  cdlemg31c  35005  cdlemk5a  35141  cdlemk5  35142  congmul  36552  jm2.25lem1  36583  jm2.26  36587  jm2.27a  36590  infleinflem1  38527  stoweidlem42  38935