Theorem syl133anc 1394

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

Syntax hints:   → wi 4   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  syl233anc  1400  mdetuni0  22105  frgrwopreg  29556  cgrtr4d  34895  cgrtrand  34903  cgrtr3and  34905  cgrcoml  34906  cgrextendand  34919  segconeu  34921  btwnouttr2  34932  cgr3tr4  34962  cgrxfr  34965  btwnxfr  34966  lineext  34986  brofs2  34987  brifs2  34988  fscgr  34990  btwnconn1lem2  34998  btwnconn1lem4  35000  btwnconn1lem8  35004  btwnconn1lem11  35007  brsegle2  35019  seglecgr12im  35020  segletr  35024  outsidele  35042  dalem13  38485  2llnma1b  38595  cdlemblem  38602  cdlemb  38603  lhpexle3  38821  lhpat  38852  4atex2-0bOLDN  38888  cdlemd4  39010  cdleme14  39082  cdleme19b  39113  cdleme20f  39123  cdleme20j  39127  cdleme20k  39128  cdleme20l2  39130  cdleme20  39133  cdleme22a  39149  cdleme22e  39153  cdleme26e  39168  cdleme28  39182  cdleme38n  39273  cdleme41sn4aw  39284  cdleme41snaw  39285  cdlemg6c  39429  cdlemg6  39432  cdlemg8c  39438  cdlemg9  39443  cdlemg10a  39449  cdlemg12c  39454  cdlemg12d  39455  cdlemg18d  39490  cdlemg18  39491  cdlemg20  39494  cdlemg21  39495  cdlemg22  39496  cdlemg28a  39502  cdlemg33b0  39510  cdlemg28b  39512  cdlemg33a  39515  cdlemg33  39520  cdlemg34  39521  cdlemg36  39523  cdlemg38  39524  cdlemg46  39544  cdlemk6  39646  cdlemki  39650  cdlemksv2  39656  cdlemk11  39658  cdlemk6u  39671  cdleml4N  39788  cdlemn11pre  40019