Theorem syl133anc 1395

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	⊢ (𝜑 → 𝜁)
syl133anc.7	⊢ (𝜑 → 𝜎)
syl133anc.8	⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)

Assertion

Ref	Expression
syl133anc	⊢ (𝜑 → 𝜌)

Proof of Theorem syl133anc

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		syl133anc.7	. . 3 ⊢ (𝜑 → 𝜎)
8	5, 6, 7	3jca 1128	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁 ∧ 𝜎))
9		syl133anc.8	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)
10	1, 2, 3, 4, 8, 9	syl131anc 1385	1 ⊢ (𝜑 → 𝜌)

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  syl233anc  1401  mdetuni0  22559  frgrwopreg  30304  cgrtr4d  36003  cgrtrand  36011  cgrtr3and  36013  cgrcoml  36014  cgrextendand  36027  segconeu  36029  btwnouttr2  36040  cgr3tr4  36070  cgrxfr  36073  btwnxfr  36074  lineext  36094  brofs2  36095  brifs2  36096  fscgr  36098  btwnconn1lem2  36106  btwnconn1lem4  36108  btwnconn1lem8  36112  btwnconn1lem11  36115  brsegle2  36127  seglecgr12im  36128  segletr  36132  outsidele  36150  dalem13  39695  2llnma1b  39805  cdlemblem  39812  cdlemb  39813  lhpexle3  40031  lhpat  40062  4atex2-0bOLDN  40098  cdlemd4  40220  cdleme14  40292  cdleme19b  40323  cdleme20f  40333  cdleme20j  40337  cdleme20k  40338  cdleme20l2  40340  cdleme20  40343  cdleme22a  40359  cdleme22e  40363  cdleme26e  40378  cdleme28  40392  cdleme38n  40483  cdleme41sn4aw  40494  cdleme41snaw  40495  cdlemg6c  40639  cdlemg6  40642  cdlemg8c  40648  cdlemg9  40653  cdlemg10a  40659  cdlemg12c  40664  cdlemg12d  40665  cdlemg18d  40700  cdlemg18  40701  cdlemg20  40704  cdlemg21  40705  cdlemg22  40706  cdlemg28a  40712  cdlemg33b0  40720  cdlemg28b  40722  cdlemg33a  40725  cdlemg33  40730  cdlemg34  40731  cdlemg36  40733  cdlemg38  40734  cdlemg46  40754  cdlemk6  40856  cdlemki  40860  cdlemksv2  40866  cdlemk11  40868  cdlemk6u  40881  cdleml4N  40998  cdlemn11pre  41229