Theorem syl133anc 1416

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  syl233anc  1422  mdetuni0  22735  frgrwopreg  30579  cgrtr4d  36343  cgrtrand  36351  cgrtr3and  36353  cgrcoml  36354  cgrextendand  36367  segconeu  36369  btwnouttr2  36380  cgr3tr4  36410  cgrxfr  36413  btwnxfr  36414  lineext  36434  brofs2  36435  brifs2  36436  fscgr  36438  btwnconn1lem2  36446  btwnconn1lem4  36448  btwnconn1lem8  36452  btwnconn1lem11  36455  brsegle2  36467  seglecgr12im  36468  segletr  36472  outsidele  36490  dalem13  40307  2llnma1b  40417  cdlemblem  40424  cdlemb  40425  lhpexle3  40643  lhpat  40674  4atex2-0bOLDN  40710  cdlemd4  40832  cdleme14  40904  cdleme19b  40935  cdleme20f  40945  cdleme20j  40949  cdleme20k  40950  cdleme20l2  40952  cdleme20  40955  cdleme22a  40971  cdleme22e  40975  cdleme26e  40990  cdleme28  41004  cdleme38n  41095  cdleme41sn4aw  41106  cdleme41snaw  41107  cdlemg6c  41251  cdlemg6  41254  cdlemg8c  41260  cdlemg9  41265  cdlemg10a  41271  cdlemg12c  41276  cdlemg12d  41277  cdlemg18d  41312  cdlemg18  41313  cdlemg20  41316  cdlemg21  41317  cdlemg22  41318  cdlemg28a  41324  cdlemg33b0  41332  cdlemg28b  41334  cdlemg33a  41337  cdlemg33  41342  cdlemg34  41343  cdlemg36  41345  cdlemg38  41346  cdlemg46  41366  cdlemk6  41468  cdlemki  41472  cdlemksv2  41478  cdlemk11  41480  cdlemk6u  41493  cdleml4N  41610  cdlemn11pre  41841