Theorem syl133anc 1516

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

Syntax hints:   → wi 4   ∧ w3a 1111

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 199  df-an 387  df-3an 1113

This theorem is referenced by:  syl233anc  1522  mdetuni0  20795  frgrwopreg  27693  cgrtr4d  32620  cgrtrand  32628  cgrtr3and  32630  cgrcoml  32631  cgrextendand  32644  segconeu  32646  btwnouttr2  32657  cgr3tr4  32687  cgrxfr  32690  btwnxfr  32691  lineext  32711  brofs2  32712  brifs2  32713  fscgr  32715  btwnconn1lem2  32723  btwnconn1lem4  32725  btwnconn1lem8  32729  btwnconn1lem11  32732  brsegle2  32744  seglecgr12im  32745  segletr  32749  outsidele  32767  dalem13  35744  2llnma1b  35854  cdlemblem  35861  cdlemb  35862  lhpexle3  36080  lhpat  36111  4atex2-0bOLDN  36147  cdlemd4  36269  cdleme14  36341  cdleme19b  36372  cdleme20f  36382  cdleme20j  36386  cdleme20k  36387  cdleme20l2  36389  cdleme20  36392  cdleme22a  36408  cdleme22e  36412  cdleme26e  36427  cdleme28  36441  cdleme38n  36532  cdleme41sn4aw  36543  cdleme41snaw  36544  cdlemg6c  36688  cdlemg6  36691  cdlemg8c  36697  cdlemg9  36702  cdlemg10a  36708  cdlemg12c  36713  cdlemg12d  36714  cdlemg18d  36749  cdlemg18  36750  cdlemg20  36753  cdlemg21  36754  cdlemg22  36755  cdlemg28a  36761  cdlemg33b0  36769  cdlemg28b  36771  cdlemg33a  36774  cdlemg33  36779  cdlemg34  36780  cdlemg36  36782  cdlemg38  36783  cdlemg46  36803  cdlemk6  36905  cdlemki  36909  cdlemksv2  36915  cdlemk11  36917  cdlemk6u  36930  cdleml4N  37047  cdlemn11pre  37278