Theorem syl133anc 1389

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  syl233anc  1395  mdetuni0  21230  frgrwopreg  28102  cgrtr4d  33446  cgrtrand  33454  cgrtr3and  33456  cgrcoml  33457  cgrextendand  33470  segconeu  33472  btwnouttr2  33483  cgr3tr4  33513  cgrxfr  33516  btwnxfr  33517  lineext  33537  brofs2  33538  brifs2  33539  fscgr  33541  btwnconn1lem2  33549  btwnconn1lem4  33551  btwnconn1lem8  33555  btwnconn1lem11  33558  brsegle2  33570  seglecgr12im  33571  segletr  33575  outsidele  33593  dalem13  36827  2llnma1b  36937  cdlemblem  36944  cdlemb  36945  lhpexle3  37163  lhpat  37194  4atex2-0bOLDN  37230  cdlemd4  37352  cdleme14  37424  cdleme19b  37455  cdleme20f  37465  cdleme20j  37469  cdleme20k  37470  cdleme20l2  37472  cdleme20  37475  cdleme22a  37491  cdleme22e  37495  cdleme26e  37510  cdleme28  37524  cdleme38n  37615  cdleme41sn4aw  37626  cdleme41snaw  37627  cdlemg6c  37771  cdlemg6  37774  cdlemg8c  37780  cdlemg9  37785  cdlemg10a  37791  cdlemg12c  37796  cdlemg12d  37797  cdlemg18d  37832  cdlemg18  37833  cdlemg20  37836  cdlemg21  37837  cdlemg22  37838  cdlemg28a  37844  cdlemg33b0  37852  cdlemg28b  37854  cdlemg33a  37857  cdlemg33  37862  cdlemg34  37863  cdlemg36  37865  cdlemg38  37866  cdlemg46  37886  cdlemk6  37988  cdlemki  37992  cdlemksv2  37998  cdlemk11  38000  cdlemk6u  38013  cdleml4N  38130  cdlemn11pre  38361