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

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  syl233anc  1426  mdetuni0  22759  frgrwopreg  30655  cgrtr4d  36458  cgrtrand  36466  cgrtr3and  36468  cgrcoml  36469  cgrextendand  36482  segconeu  36484  btwnouttr2  36495  cgr3tr4  36525  cgrxfr  36528  btwnxfr  36529  lineext  36549  brofs2  36550  brifs2  36551  fscgr  36553  btwnconn1lem2  36561  btwnconn1lem4  36563  btwnconn1lem8  36567  btwnconn1lem11  36570  brsegle2  36582  seglecgr12im  36583  segletr  36587  outsidele  36605  dalem13  40431  2llnma1b  40541  cdlemblem  40548  cdlemb  40549  lhpexle3  40767  lhpat  40798  4atex2-0bOLDN  40834  cdlemd4  40956  cdleme14  41028  cdleme19b  41059  cdleme20f  41069  cdleme20j  41073  cdleme20k  41074  cdleme20l2  41076  cdleme20  41079  cdleme22a  41095  cdleme22e  41099  cdleme26e  41114  cdleme28  41128  cdleme38n  41219  cdleme41sn4aw  41230  cdleme41snaw  41231  cdlemg6c  41375  cdlemg6  41378  cdlemg8c  41384  cdlemg9  41389  cdlemg10a  41395  cdlemg12c  41400  cdlemg12d  41401  cdlemg18d  41436  cdlemg18  41437  cdlemg20  41440  cdlemg21  41441  cdlemg22  41442  cdlemg28a  41448  cdlemg33b0  41456  cdlemg28b  41458  cdlemg33a  41461  cdlemg33  41466  cdlemg34  41467  cdlemg36  41469  cdlemg38  41470  cdlemg46  41490  cdlemk6  41592  cdlemki  41596  cdlemksv2  41602  cdlemk11  41604  cdlemk6u  41617  cdleml4N  41734  cdlemn11pre  41965