Theorem syl133anc 1420

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl233anc  1426  mdetuni0  22916  frgrwopreg  30906  cgrtr4d  36720  cgrtrand  36728  cgrtr3and  36730  cgrcoml  36731  cgrextendand  36744  segconeu  36746  btwnouttr2  36757  cgr3tr4  36787  cgrxfr  36790  btwnxfr  36791  lineext  36811  brofs2  36812  brifs2  36813  fscgr  36815  btwnconn1lem2  36823  btwnconn1lem4  36825  btwnconn1lem8  36829  btwnconn1lem11  36832  brsegle2  36844  seglecgr12im  36845  segletr  36849  outsidele  36867  dalem13  40701  2llnma1b  40811  cdlemblem  40818  cdlemb  40819  lhpexle3  41037  lhpat  41068  4atex2-0bOLDN  41104  cdlemd4  41226  cdleme14  41298  cdleme19b  41329  cdleme20f  41339  cdleme20j  41343  cdleme20k  41344  cdleme20l2  41346  cdleme20  41349  cdleme22a  41365  cdleme22e  41369  cdleme26e  41384  cdleme28  41398  cdleme38n  41489  cdleme41sn4aw  41500  cdleme41snaw  41501  cdlemg6c  41645  cdlemg6  41648  cdlemg8c  41654  cdlemg9  41659  cdlemg10a  41665  cdlemg12c  41670  cdlemg12d  41671  cdlemg18d  41706  cdlemg18  41707  cdlemg20  41710  cdlemg21  41711  cdlemg22  41712  cdlemg28a  41718  cdlemg33b0  41726  cdlemg28b  41728  cdlemg33a  41731  cdlemg33  41736  cdlemg34  41737  cdlemg36  41739  cdlemg38  41740  cdlemg46  41760  cdlemk6  41862  cdlemki  41866  cdlemksv2  41872  cdlemk11  41874  cdlemk6u  41887  cdleml4N  42004  cdlemn11pre  42235