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  22524  frgrwopreg  30285  cgrtr4d  35961  cgrtrand  35969  cgrtr3and  35971  cgrcoml  35972  cgrextendand  35985  segconeu  35987  btwnouttr2  35998  cgr3tr4  36028  cgrxfr  36031  btwnxfr  36032  lineext  36052  brofs2  36053  brifs2  36054  fscgr  36056  btwnconn1lem2  36064  btwnconn1lem4  36066  btwnconn1lem8  36070  btwnconn1lem11  36073  brsegle2  36085  seglecgr12im  36086  segletr  36090  outsidele  36108  dalem13  39658  2llnma1b  39768  cdlemblem  39775  cdlemb  39776  lhpexle3  39994  lhpat  40025  4atex2-0bOLDN  40061  cdlemd4  40183  cdleme14  40255  cdleme19b  40286  cdleme20f  40296  cdleme20j  40300  cdleme20k  40301  cdleme20l2  40303  cdleme20  40306  cdleme22a  40322  cdleme22e  40326  cdleme26e  40341  cdleme28  40355  cdleme38n  40446  cdleme41sn4aw  40457  cdleme41snaw  40458  cdlemg6c  40602  cdlemg6  40605  cdlemg8c  40611  cdlemg9  40616  cdlemg10a  40622  cdlemg12c  40627  cdlemg12d  40628  cdlemg18d  40663  cdlemg18  40664  cdlemg20  40667  cdlemg21  40668  cdlemg22  40669  cdlemg28a  40675  cdlemg33b0  40683  cdlemg28b  40685  cdlemg33a  40688  cdlemg33  40693  cdlemg34  40694  cdlemg36  40696  cdlemg38  40697  cdlemg46  40717  cdlemk6  40819  cdlemki  40823  cdlemksv2  40829  cdlemk11  40831  cdlemk6u  40844  cdleml4N  40961  cdlemn11pre  41192