Theorem syl222anc 1413

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anandis  1500  3anandirs  1501  omopth2  8596  omeu  8597  dfac12lem2  10227  xaddass2  13384  xpncan  13385  divdenle  16931  pockthlem  17089  znidomb  21873  tanord1  26871  ang180lem5  27147  isosctrlem3  27154  log2tlbnd  27279  basellem1  27414  perfectlem2  27563  bposlem6  27622  dchrisum0flblem2  27842  pntpbnd1a  27918  mulsproplem1  28508  axcontlem8  29555  xlt2addrd  33398  s2f1  33557  xrge0addass  33624  xrge0npcan  33628  elrgspnlem1  33850  submatminr1  34489  carsgclctunlem2  34998  nmulss1  37056  nadddilem3  37064  4atexlemntlpq  41219  4atexlemnclw  41221  trlval2  41314  cdleme0moN  41376  cdleme16b  41430  cdleme16c  41431  cdleme16d  41432  cdleme16e  41433  cdleme17c  41439  cdlemeda  41449  cdleme20h  41467  cdleme20j  41469  cdleme20l2  41472  cdleme21c  41478  cdleme21ct  41480  cdleme22aa  41490  cdleme22cN  41493  cdleme22d  41494  cdleme22e  41495  cdleme22eALTN  41496  cdleme23b  41501  cdleme25a  41504  cdleme25dN  41507  cdleme27N  41520  cdleme28a  41521  cdleme28b  41522  cdleme29ex  41525  cdleme32c  41594  cdleme42k  41635  cdlemg2cex  41742  cdlemg2idN  41747  cdlemg31c  41850  cdlemk5a  41986  cdlemk5  41987  congmul  44068  jm2.25lem1  44099  jm2.26  44103  jm2.27a  44106  infleinflem1  46475  stoweidlem42  47146