Theorem syl133anc 1391

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 1126	. 2 ⊢ (𝜑 → (𝜂 ∧ 𝜁 ∧ 𝜎))
9		syl133anc.8	. 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌)
10	1, 2, 3, 4, 8, 9	syl131anc 1381	1 ⊢ (𝜑 → 𝜌)

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  syl233anc  1397  mdetuni0  21678  frgrwopreg  28588  cgrtr4d  34214  cgrtrand  34222  cgrtr3and  34224  cgrcoml  34225  cgrextendand  34238  segconeu  34240  btwnouttr2  34251  cgr3tr4  34281  cgrxfr  34284  btwnxfr  34285  lineext  34305  brofs2  34306  brifs2  34307  fscgr  34309  btwnconn1lem2  34317  btwnconn1lem4  34319  btwnconn1lem8  34323  btwnconn1lem11  34326  brsegle2  34338  seglecgr12im  34339  segletr  34343  outsidele  34361  dalem13  37617  2llnma1b  37727  cdlemblem  37734  cdlemb  37735  lhpexle3  37953  lhpat  37984  4atex2-0bOLDN  38020  cdlemd4  38142  cdleme14  38214  cdleme19b  38245  cdleme20f  38255  cdleme20j  38259  cdleme20k  38260  cdleme20l2  38262  cdleme20  38265  cdleme22a  38281  cdleme22e  38285  cdleme26e  38300  cdleme28  38314  cdleme38n  38405  cdleme41sn4aw  38416  cdleme41snaw  38417  cdlemg6c  38561  cdlemg6  38564  cdlemg8c  38570  cdlemg9  38575  cdlemg10a  38581  cdlemg12c  38586  cdlemg12d  38587  cdlemg18d  38622  cdlemg18  38623  cdlemg20  38626  cdlemg21  38627  cdlemg22  38628  cdlemg28a  38634  cdlemg33b0  38642  cdlemg28b  38644  cdlemg33a  38647  cdlemg33  38652  cdlemg34  38653  cdlemg36  38655  cdlemg38  38656  cdlemg46  38676  cdlemk6  38778  cdlemki  38782  cdlemksv2  38788  cdlemk11  38790  cdlemk6u  38803  cdleml4N  38920  cdlemn11pre  39151