Theorem syl133anc 1392

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 1127	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁 ∧ 𝜎))
9		syl133anc.8	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)
10	1, 2, 3, 4, 8, 9	syl131anc 1382	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  1398  mdetuni0  22643  frgrwopreg  30352  cgrtr4d  35967  cgrtrand  35975  cgrtr3and  35977  cgrcoml  35978  cgrextendand  35991  segconeu  35993  btwnouttr2  36004  cgr3tr4  36034  cgrxfr  36037  btwnxfr  36038  lineext  36058  brofs2  36059  brifs2  36060  fscgr  36062  btwnconn1lem2  36070  btwnconn1lem4  36072  btwnconn1lem8  36076  btwnconn1lem11  36079  brsegle2  36091  seglecgr12im  36092  segletr  36096  outsidele  36114  dalem13  39659  2llnma1b  39769  cdlemblem  39776  cdlemb  39777  lhpexle3  39995  lhpat  40026  4atex2-0bOLDN  40062  cdlemd4  40184  cdleme14  40256  cdleme19b  40287  cdleme20f  40297  cdleme20j  40301  cdleme20k  40302  cdleme20l2  40304  cdleme20  40307  cdleme22a  40323  cdleme22e  40327  cdleme26e  40342  cdleme28  40356  cdleme38n  40447  cdleme41sn4aw  40458  cdleme41snaw  40459  cdlemg6c  40603  cdlemg6  40606  cdlemg8c  40612  cdlemg9  40617  cdlemg10a  40623  cdlemg12c  40628  cdlemg12d  40629  cdlemg18d  40664  cdlemg18  40665  cdlemg20  40668  cdlemg21  40669  cdlemg22  40670  cdlemg28a  40676  cdlemg33b0  40684  cdlemg28b  40686  cdlemg33a  40689  cdlemg33  40694  cdlemg34  40695  cdlemg36  40697  cdlemg38  40698  cdlemg46  40718  cdlemk6  40820  cdlemki  40824  cdlemksv2  40830  cdlemk11  40832  cdlemk6u  40845  cdleml4N  40962  cdlemn11pre  41193