Theorem syl133anc 1420

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

This proof depends on syntax axioms:   → wi 4   ∧ 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:  syl233anc  1426  mdetuni0  22942  frgrwopreg  30930  cgrtr4d  36843  cgrtrand  36851  cgrtr3and  36853  cgrcoml  36854  cgrextendand  36867  segconeu  36869  btwnouttr2  36880  cgr3tr4  36910  cgrxfr  36913  btwnxfr  36914  lineext  36934  brofs2  36935  brifs2  36936  fscgr  36938  btwnconn1lem2  36946  btwnconn1lem4  36948  btwnconn1lem8  36952  btwnconn1lem11  36955  brsegle2  36967  seglecgr12im  36968  segletr  36972  outsidele  36990  dalem13  40827  2llnma1b  40937  cdlemblem  40944  cdlemb  40945  lhpexle3  41163  lhpat  41194  4atex2-0bOLDN  41230  cdlemd4  41352  cdleme14  41424  cdleme19b  41455  cdleme20f  41465  cdleme20j  41469  cdleme20k  41470  cdleme20l2  41472  cdleme20  41475  cdleme22a  41491  cdleme22e  41495  cdleme26e  41510  cdleme28  41524  cdleme38n  41615  cdleme41sn4aw  41626  cdleme41snaw  41627  cdlemg6c  41771  cdlemg6  41774  cdlemg8c  41780  cdlemg9  41785  cdlemg10a  41791  cdlemg12c  41796  cdlemg12d  41797  cdlemg18d  41832  cdlemg18  41833  cdlemg20  41836  cdlemg21  41837  cdlemg22  41838  cdlemg28a  41844  cdlemg33b0  41852  cdlemg28b  41854  cdlemg33a  41857  cdlemg33  41862  cdlemg34  41863  cdlemg36  41865  cdlemg38  41866  cdlemg46  41886  cdlemk6  41988  cdlemki  41992  cdlemksv2  41998  cdlemk11  42000  cdlemk6u  42013  cdleml4N  42130  cdlemn11pre  42361