Theorem syl222anc 1383

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  3anandis  1468  3anandirs  1469  omopth2  8193  omeu  8194  dfac12lem2  9555  xaddass2  12631  xpncan  12632  divdenle  16079  pockthlem  16231  znidomb  20253  tanord1  25129  ang180lem5  25399  isosctrlem3  25406  log2tlbnd  25531  basellem1  25666  perfectlem2  25814  bposlem6  25873  dchrisum0flblem2  26093  pntpbnd1a  26169  axcontlem8  26765  xlt2addrd  30508  s2f1  30647  xrge0addass  30724  xrge0npcan  30728  submatminr1  31163  carsgclctunlem2  31687  4atexlemntlpq  37364  4atexlemnclw  37366  trlval2  37459  cdleme0moN  37521  cdleme16b  37575  cdleme16c  37576  cdleme16d  37577  cdleme16e  37578  cdleme17c  37584  cdlemeda  37594  cdleme20h  37612  cdleme20j  37614  cdleme20l2  37617  cdleme21c  37623  cdleme21ct  37625  cdleme22aa  37635  cdleme22cN  37638  cdleme22d  37639  cdleme22e  37640  cdleme22eALTN  37641  cdleme23b  37646  cdleme25a  37649  cdleme25dN  37652  cdleme27N  37665  cdleme28a  37666  cdleme28b  37667  cdleme29ex  37670  cdleme32c  37739  cdleme42k  37780  cdlemg2cex  37887  cdlemg2idN  37892  cdlemg31c  37995  cdlemk5a  38131  cdlemk5  38132  congmul  39908  jm2.25lem1  39939  jm2.26  39943  jm2.27a  39946  infleinflem1  42002  stoweidlem42  42684