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  22565  frgrwopreg  30398  cgrtr4d  36179  cgrtrand  36187  cgrtr3and  36189  cgrcoml  36190  cgrextendand  36203  segconeu  36205  btwnouttr2  36216  cgr3tr4  36246  cgrxfr  36249  btwnxfr  36250  lineext  36270  brofs2  36271  brifs2  36272  fscgr  36274  btwnconn1lem2  36282  btwnconn1lem4  36284  btwnconn1lem8  36288  btwnconn1lem11  36291  brsegle2  36303  seglecgr12im  36304  segletr  36308  outsidele  36326  dalem13  39936  2llnma1b  40046  cdlemblem  40053  cdlemb  40054  lhpexle3  40272  lhpat  40303  4atex2-0bOLDN  40339  cdlemd4  40461  cdleme14  40533  cdleme19b  40564  cdleme20f  40574  cdleme20j  40578  cdleme20k  40579  cdleme20l2  40581  cdleme20  40584  cdleme22a  40600  cdleme22e  40604  cdleme26e  40619  cdleme28  40633  cdleme38n  40724  cdleme41sn4aw  40735  cdleme41snaw  40736  cdlemg6c  40880  cdlemg6  40883  cdlemg8c  40889  cdlemg9  40894  cdlemg10a  40900  cdlemg12c  40905  cdlemg12d  40906  cdlemg18d  40941  cdlemg18  40942  cdlemg20  40945  cdlemg21  40946  cdlemg22  40947  cdlemg28a  40953  cdlemg33b0  40961  cdlemg28b  40963  cdlemg33a  40966  cdlemg33  40971  cdlemg34  40972  cdlemg36  40974  cdlemg38  40975  cdlemg46  40995  cdlemk6  41097  cdlemki  41101  cdlemksv2  41107  cdlemk11  41109  cdlemk6u  41122  cdleml4N  41239  cdlemn11pre  41470