Theorem syl133anc 1390

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  syl233anc  1396  mdetuni0  21226  frgrwopreg  28108  cgrtr4d  33559  cgrtrand  33567  cgrtr3and  33569  cgrcoml  33570  cgrextendand  33583  segconeu  33585  btwnouttr2  33596  cgr3tr4  33626  cgrxfr  33629  btwnxfr  33630  lineext  33650  brofs2  33651  brifs2  33652  fscgr  33654  btwnconn1lem2  33662  btwnconn1lem4  33664  btwnconn1lem8  33668  btwnconn1lem11  33671  brsegle2  33683  seglecgr12im  33684  segletr  33688  outsidele  33706  dalem13  36972  2llnma1b  37082  cdlemblem  37089  cdlemb  37090  lhpexle3  37308  lhpat  37339  4atex2-0bOLDN  37375  cdlemd4  37497  cdleme14  37569  cdleme19b  37600  cdleme20f  37610  cdleme20j  37614  cdleme20k  37615  cdleme20l2  37617  cdleme20  37620  cdleme22a  37636  cdleme22e  37640  cdleme26e  37655  cdleme28  37669  cdleme38n  37760  cdleme41sn4aw  37771  cdleme41snaw  37772  cdlemg6c  37916  cdlemg6  37919  cdlemg8c  37925  cdlemg9  37930  cdlemg10a  37936  cdlemg12c  37941  cdlemg12d  37942  cdlemg18d  37977  cdlemg18  37978  cdlemg20  37981  cdlemg21  37982  cdlemg22  37983  cdlemg28a  37989  cdlemg33b0  37997  cdlemg28b  37999  cdlemg33a  38002  cdlemg33  38007  cdlemg34  38008  cdlemg36  38010  cdlemg38  38011  cdlemg46  38031  cdlemk6  38133  cdlemki  38137  cdlemksv2  38143  cdlemk11  38145  cdlemk6u  38158  cdleml4N  38275  cdlemn11pre  38506