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  22508  frgrwopreg  30252  cgrtr4d  35973  cgrtrand  35981  cgrtr3and  35983  cgrcoml  35984  cgrextendand  35997  segconeu  35999  btwnouttr2  36010  cgr3tr4  36040  cgrxfr  36043  btwnxfr  36044  lineext  36064  brofs2  36065  brifs2  36066  fscgr  36068  btwnconn1lem2  36076  btwnconn1lem4  36078  btwnconn1lem8  36082  btwnconn1lem11  36085  brsegle2  36097  seglecgr12im  36098  segletr  36102  outsidele  36120  dalem13  39670  2llnma1b  39780  cdlemblem  39787  cdlemb  39788  lhpexle3  40006  lhpat  40037  4atex2-0bOLDN  40073  cdlemd4  40195  cdleme14  40267  cdleme19b  40298  cdleme20f  40308  cdleme20j  40312  cdleme20k  40313  cdleme20l2  40315  cdleme20  40318  cdleme22a  40334  cdleme22e  40338  cdleme26e  40353  cdleme28  40367  cdleme38n  40458  cdleme41sn4aw  40469  cdleme41snaw  40470  cdlemg6c  40614  cdlemg6  40617  cdlemg8c  40623  cdlemg9  40628  cdlemg10a  40634  cdlemg12c  40639  cdlemg12d  40640  cdlemg18d  40675  cdlemg18  40676  cdlemg20  40679  cdlemg21  40680  cdlemg22  40681  cdlemg28a  40687  cdlemg33b0  40695  cdlemg28b  40697  cdlemg33a  40700  cdlemg33  40705  cdlemg34  40706  cdlemg36  40708  cdlemg38  40709  cdlemg46  40729  cdlemk6  40831  cdlemki  40835  cdlemksv2  40841  cdlemk11  40843  cdlemk6u  40856  cdleml4N  40973  cdlemn11pre  41204