Theorem syl133anc 1393

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 1383	1 ⊢ (𝜑 → 𝜌)

Syntax hints:   → wi 4   ∧ w3a 1087

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

This theorem is referenced by:  syl233anc  1399  mdetuni0  22130  frgrwopreg  29614  cgrtr4d  35026  cgrtrand  35034  cgrtr3and  35036  cgrcoml  35037  cgrextendand  35050  segconeu  35052  btwnouttr2  35063  cgr3tr4  35093  cgrxfr  35096  btwnxfr  35097  lineext  35117  brofs2  35118  brifs2  35119  fscgr  35121  btwnconn1lem2  35129  btwnconn1lem4  35131  btwnconn1lem8  35135  btwnconn1lem11  35138  brsegle2  35150  seglecgr12im  35151  segletr  35155  outsidele  35173  dalem13  38633  2llnma1b  38743  cdlemblem  38750  cdlemb  38751  lhpexle3  38969  lhpat  39000  4atex2-0bOLDN  39036  cdlemd4  39158  cdleme14  39230  cdleme19b  39261  cdleme20f  39271  cdleme20j  39275  cdleme20k  39276  cdleme20l2  39278  cdleme20  39281  cdleme22a  39297  cdleme22e  39301  cdleme26e  39316  cdleme28  39330  cdleme38n  39421  cdleme41sn4aw  39432  cdleme41snaw  39433  cdlemg6c  39577  cdlemg6  39580  cdlemg8c  39586  cdlemg9  39591  cdlemg10a  39597  cdlemg12c  39602  cdlemg12d  39603  cdlemg18d  39638  cdlemg18  39639  cdlemg20  39642  cdlemg21  39643  cdlemg22  39644  cdlemg28a  39650  cdlemg33b0  39658  cdlemg28b  39660  cdlemg33a  39663  cdlemg33  39668  cdlemg34  39669  cdlemg36  39671  cdlemg38  39672  cdlemg46  39692  cdlemk6  39794  cdlemki  39798  cdlemksv2  39804  cdlemk11  39806  cdlemk6u  39819  cdleml4N  39936  cdlemn11pre  40167