Theorem syl222anc 1404

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

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

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  3anandis  1491  3anandirs  1492  omopth2  8546  omeu  8547  dfac12lem2  10094  xaddass2  13246  xpncan  13247  divdenle  16774  pockthlem  16931  znidomb  21600  tanord1  26589  ang180lem5  26865  isosctrlem3  26872  log2tlbnd  26997  basellem1  27132  perfectlem2  27281  bposlem6  27340  dchrisum0flblem2  27560  pntpbnd1a  27636  mulsproplem1  28196  axcontlem8  29128  xlt2addrd  32921  s2f1  33083  xrge0addass  33154  xrge0npcan  33158  elrgspnlem1  33383  submatminr1  34067  carsgclctunlem2  34576  4atexlemntlpq  40652  4atexlemnclw  40654  trlval2  40747  cdleme0moN  40809  cdleme16b  40863  cdleme16c  40864  cdleme16d  40865  cdleme16e  40866  cdleme17c  40872  cdlemeda  40882  cdleme20h  40900  cdleme20j  40902  cdleme20l2  40905  cdleme21c  40911  cdleme21ct  40913  cdleme22aa  40923  cdleme22cN  40926  cdleme22d  40927  cdleme22e  40928  cdleme22eALTN  40929  cdleme23b  40934  cdleme25a  40937  cdleme25dN  40940  cdleme27N  40953  cdleme28a  40954  cdleme28b  40955  cdleme29ex  40958  cdleme32c  41027  cdleme42k  41068  cdlemg2cex  41175  cdlemg2idN  41180  cdlemg31c  41283  cdlemk5a  41419  cdlemk5  41420  congmul  43504  jm2.25lem1  43535  jm2.26  43539  jm2.27a  43542  infleinflem1  45905  stoweidlem42  46576