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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl233anc  1426  mdetuni0  22849  frgrwopreg  30811  cgrtr4d  36573  cgrtrand  36581  cgrtr3and  36583  cgrcoml  36584  cgrextendand  36597  segconeu  36599  btwnouttr2  36610  cgr3tr4  36640  cgrxfr  36643  btwnxfr  36644  lineext  36664  brofs2  36665  brifs2  36666  fscgr  36668  btwnconn1lem2  36676  btwnconn1lem4  36678  btwnconn1lem8  36682  btwnconn1lem11  36685  brsegle2  36697  seglecgr12im  36698  segletr  36702  outsidele  36720  dalem13  40557  2llnma1b  40667  cdlemblem  40674  cdlemb  40675  lhpexle3  40893  lhpat  40924  4atex2-0bOLDN  40960  cdlemd4  41082  cdleme14  41154  cdleme19b  41185  cdleme20f  41195  cdleme20j  41199  cdleme20k  41200  cdleme20l2  41202  cdleme20  41205  cdleme22a  41221  cdleme22e  41225  cdleme26e  41240  cdleme28  41254  cdleme38n  41345  cdleme41sn4aw  41356  cdleme41snaw  41357  cdlemg6c  41501  cdlemg6  41504  cdlemg8c  41510  cdlemg9  41515  cdlemg10a  41521  cdlemg12c  41526  cdlemg12d  41527  cdlemg18d  41562  cdlemg18  41563  cdlemg20  41566  cdlemg21  41567  cdlemg22  41568  cdlemg28a  41574  cdlemg33b0  41582  cdlemg28b  41584  cdlemg33a  41587  cdlemg33  41592  cdlemg34  41593  cdlemg36  41595  cdlemg38  41596  cdlemg46  41616  cdlemk6  41718  cdlemki  41722  cdlemksv2  41728  cdlemk11  41730  cdlemk6u  41743  cdleml4N  41860  cdlemn11pre  42091