![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl123anc | 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 | ⊢ (𝜑 → 𝜁) |
syl123anc.7 | ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) |
Ref | Expression |
---|---|
syl123anc | ⊢ (𝜑 → 𝜎) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3anc.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | syl3anc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | syl3anc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | 2, 3 | jca 513 | . 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃)) |
5 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl33anc.6 | . 2 ⊢ (𝜑 → 𝜁) | |
8 | syl123anc.7 | . 2 ⊢ ((𝜓 ∧ (𝜒 ∧ 𝜃) ∧ (𝜏 ∧ 𝜂 ∧ 𝜁)) → 𝜎) | |
9 | 1, 4, 5, 6, 7, 8 | syl113anc 1383 | 1 ⊢ (𝜑 → 𝜎) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∧ 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: dvfsumlem2 25544 noinfbnd2 27234 gg-dvfsumlem2 35183 atbtwnexOLDN 38318 atbtwnex 38319 osumcllem7N 38833 lhpmcvr5N 38898 cdleme22f2 39218 cdlemefs32sn1aw 39285 cdlemg7aN 39496 cdlemg7N 39497 cdlemg8c 39500 cdlemg8 39502 cdlemg11aq 39509 cdlemg12b 39515 cdlemg12e 39518 cdlemg12g 39520 cdlemg13a 39522 cdlemg15a 39526 cdlemg17e 39536 cdlemg18d 39552 cdlemg19a 39554 cdlemg20 39556 cdlemg22 39558 cdlemg28a 39564 cdlemg29 39576 cdlemg44a 39602 cdlemk34 39781 cdlemn11pre 40081 dihord10 40094 dihord2pre 40096 dihmeetlem17N 40194 |
Copyright terms: Public domain | W3C validator |