Theorem syl133anc 1395

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  syl233anc  1401  mdetuni0  22539  frgrwopreg  30307  cgrtr4d  36052  cgrtrand  36060  cgrtr3and  36062  cgrcoml  36063  cgrextendand  36076  segconeu  36078  btwnouttr2  36089  cgr3tr4  36119  cgrxfr  36122  btwnxfr  36123  lineext  36143  brofs2  36144  brifs2  36145  fscgr  36147  btwnconn1lem2  36155  btwnconn1lem4  36157  btwnconn1lem8  36161  btwnconn1lem11  36164  brsegle2  36176  seglecgr12im  36177  segletr  36181  outsidele  36199  dalem13  39798  2llnma1b  39908  cdlemblem  39915  cdlemb  39916  lhpexle3  40134  lhpat  40165  4atex2-0bOLDN  40201  cdlemd4  40323  cdleme14  40395  cdleme19b  40426  cdleme20f  40436  cdleme20j  40440  cdleme20k  40441  cdleme20l2  40443  cdleme20  40446  cdleme22a  40462  cdleme22e  40466  cdleme26e  40481  cdleme28  40495  cdleme38n  40586  cdleme41sn4aw  40597  cdleme41snaw  40598  cdlemg6c  40742  cdlemg6  40745  cdlemg8c  40751  cdlemg9  40756  cdlemg10a  40762  cdlemg12c  40767  cdlemg12d  40768  cdlemg18d  40803  cdlemg18  40804  cdlemg20  40807  cdlemg21  40808  cdlemg22  40809  cdlemg28a  40815  cdlemg33b0  40823  cdlemg28b  40825  cdlemg33a  40828  cdlemg33  40833  cdlemg34  40834  cdlemg36  40836  cdlemg38  40837  cdlemg46  40857  cdlemk6  40959  cdlemki  40963  cdlemksv2  40969  cdlemk11  40971  cdlemk6u  40984  cdleml4N  41101  cdlemn11pre  41332