Theorem syl133anc 1401

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  syl233anc  1407  mdetuni0  22611  frgrwopreg  30418  cgrtr4d  36220  cgrtrand  36228  cgrtr3and  36230  cgrcoml  36231  cgrextendand  36244  segconeu  36246  btwnouttr2  36257  cgr3tr4  36287  cgrxfr  36290  btwnxfr  36291  lineext  36311  brofs2  36312  brifs2  36313  fscgr  36315  btwnconn1lem2  36323  btwnconn1lem4  36325  btwnconn1lem8  36329  btwnconn1lem11  36332  brsegle2  36344  seglecgr12im  36345  segletr  36349  outsidele  36367  dalem13  40175  2llnma1b  40285  cdlemblem  40292  cdlemb  40293  lhpexle3  40511  lhpat  40542  4atex2-0bOLDN  40578  cdlemd4  40700  cdleme14  40772  cdleme19b  40803  cdleme20f  40813  cdleme20j  40817  cdleme20k  40818  cdleme20l2  40820  cdleme20  40823  cdleme22a  40839  cdleme22e  40843  cdleme26e  40858  cdleme28  40872  cdleme38n  40963  cdleme41sn4aw  40974  cdleme41snaw  40975  cdlemg6c  41119  cdlemg6  41122  cdlemg8c  41128  cdlemg9  41133  cdlemg10a  41139  cdlemg12c  41144  cdlemg12d  41145  cdlemg18d  41180  cdlemg18  41181  cdlemg20  41184  cdlemg21  41185  cdlemg22  41186  cdlemg28a  41192  cdlemg33b0  41200  cdlemg28b  41202  cdlemg33a  41205  cdlemg33  41210  cdlemg34  41211  cdlemg36  41213  cdlemg38  41214  cdlemg46  41234  cdlemk6  41336  cdlemki  41340  cdlemksv2  41346  cdlemk11  41348  cdlemk6u  41361  cdleml4N  41478  cdlemn11pre  41709