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  22123  frgrwopreg  29576  cgrtr4d  34957  cgrtrand  34965  cgrtr3and  34967  cgrcoml  34968  cgrextendand  34981  segconeu  34983  btwnouttr2  34994  cgr3tr4  35024  cgrxfr  35027  btwnxfr  35028  lineext  35048  brofs2  35049  brifs2  35050  fscgr  35052  btwnconn1lem2  35060  btwnconn1lem4  35062  btwnconn1lem8  35066  btwnconn1lem11  35069  brsegle2  35081  seglecgr12im  35082  segletr  35086  outsidele  35104  dalem13  38547  2llnma1b  38657  cdlemblem  38664  cdlemb  38665  lhpexle3  38883  lhpat  38914  4atex2-0bOLDN  38950  cdlemd4  39072  cdleme14  39144  cdleme19b  39175  cdleme20f  39185  cdleme20j  39189  cdleme20k  39190  cdleme20l2  39192  cdleme20  39195  cdleme22a  39211  cdleme22e  39215  cdleme26e  39230  cdleme28  39244  cdleme38n  39335  cdleme41sn4aw  39346  cdleme41snaw  39347  cdlemg6c  39491  cdlemg6  39494  cdlemg8c  39500  cdlemg9  39505  cdlemg10a  39511  cdlemg12c  39516  cdlemg12d  39517  cdlemg18d  39552  cdlemg18  39553  cdlemg20  39556  cdlemg21  39557  cdlemg22  39558  cdlemg28a  39564  cdlemg33b0  39572  cdlemg28b  39574  cdlemg33a  39577  cdlemg33  39582  cdlemg34  39583  cdlemg36  39585  cdlemg38  39586  cdlemg46  39606  cdlemk6  39708  cdlemki  39712  cdlemksv2  39718  cdlemk11  39720  cdlemk6u  39733  cdleml4N  39850  cdlemn11pre  40081