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 1129	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁 ∧ 𝜎))
9		syl133anc.8	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)
10	1, 2, 3, 4, 8, 9	syl131anc 1385	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 207  df-an 396  df-3an 1089

This theorem is referenced by:  syl233anc  1401  mdetuni0  22627  frgrwopreg  30342  cgrtr4d  35986  cgrtrand  35994  cgrtr3and  35996  cgrcoml  35997  cgrextendand  36010  segconeu  36012  btwnouttr2  36023  cgr3tr4  36053  cgrxfr  36056  btwnxfr  36057  lineext  36077  brofs2  36078  brifs2  36079  fscgr  36081  btwnconn1lem2  36089  btwnconn1lem4  36091  btwnconn1lem8  36095  btwnconn1lem11  36098  brsegle2  36110  seglecgr12im  36111  segletr  36115  outsidele  36133  dalem13  39678  2llnma1b  39788  cdlemblem  39795  cdlemb  39796  lhpexle3  40014  lhpat  40045  4atex2-0bOLDN  40081  cdlemd4  40203  cdleme14  40275  cdleme19b  40306  cdleme20f  40316  cdleme20j  40320  cdleme20k  40321  cdleme20l2  40323  cdleme20  40326  cdleme22a  40342  cdleme22e  40346  cdleme26e  40361  cdleme28  40375  cdleme38n  40466  cdleme41sn4aw  40477  cdleme41snaw  40478  cdlemg6c  40622  cdlemg6  40625  cdlemg8c  40631  cdlemg9  40636  cdlemg10a  40642  cdlemg12c  40647  cdlemg12d  40648  cdlemg18d  40683  cdlemg18  40684  cdlemg20  40687  cdlemg21  40688  cdlemg22  40689  cdlemg28a  40695  cdlemg33b0  40703  cdlemg28b  40705  cdlemg33a  40708  cdlemg33  40713  cdlemg34  40714  cdlemg36  40716  cdlemg38  40717  cdlemg46  40737  cdlemk6  40839  cdlemki  40843  cdlemksv2  40849  cdlemk11  40851  cdlemk6u  40864  cdleml4N  40981  cdlemn11pre  41212