![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl133anc | Structured version Visualization version GIF version |
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.) |
Ref | Expression |
---|---|
syl3anc.1 | ⊢ (𝜑 → 𝜓) |
syl3anc.2 | ⊢ (𝜑 → 𝜒) |
syl3anc.3 | ⊢ (𝜑 → 𝜃) |
syl3Xanc.4 | ⊢ (𝜑 → 𝜏) |
syl23anc.5 | ⊢ (𝜑 → 𝜂) |
syl33anc.6 | ⊢ (𝜑 → 𝜁) |
syl133anc.7 | ⊢ (𝜑 → 𝜎) |
syl133anc.8 | ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃 ∧ 𝜏) ∧ (𝜂 ∧ 𝜁 ∧ 𝜎)) → 𝜌) |
Ref | Expression |
---|---|
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 1384 | 1 ⊢ (𝜑 → 𝜌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1088 |
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 398 df-3an 1090 |
This theorem is referenced by: syl233anc 1400 mdetuni0 22105 frgrwopreg 29556 cgrtr4d 34895 cgrtrand 34903 cgrtr3and 34905 cgrcoml 34906 cgrextendand 34919 segconeu 34921 btwnouttr2 34932 cgr3tr4 34962 cgrxfr 34965 btwnxfr 34966 lineext 34986 brofs2 34987 brifs2 34988 fscgr 34990 btwnconn1lem2 34998 btwnconn1lem4 35000 btwnconn1lem8 35004 btwnconn1lem11 35007 brsegle2 35019 seglecgr12im 35020 segletr 35024 outsidele 35042 dalem13 38485 2llnma1b 38595 cdlemblem 38602 cdlemb 38603 lhpexle3 38821 lhpat 38852 4atex2-0bOLDN 38888 cdlemd4 39010 cdleme14 39082 cdleme19b 39113 cdleme20f 39123 cdleme20j 39127 cdleme20k 39128 cdleme20l2 39130 cdleme20 39133 cdleme22a 39149 cdleme22e 39153 cdleme26e 39168 cdleme28 39182 cdleme38n 39273 cdleme41sn4aw 39284 cdleme41snaw 39285 cdlemg6c 39429 cdlemg6 39432 cdlemg8c 39438 cdlemg9 39443 cdlemg10a 39449 cdlemg12c 39454 cdlemg12d 39455 cdlemg18d 39490 cdlemg18 39491 cdlemg20 39494 cdlemg21 39495 cdlemg22 39496 cdlemg28a 39502 cdlemg33b0 39510 cdlemg28b 39512 cdlemg33a 39515 cdlemg33 39520 cdlemg34 39521 cdlemg36 39523 cdlemg38 39524 cdlemg46 39544 cdlemk6 39646 cdlemki 39650 cdlemksv2 39656 cdlemk11 39658 cdlemk6u 39671 cdleml4N 39788 cdlemn11pre 40019 |
Copyright terms: Public domain | W3C validator |