![]() |
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 510 | . 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 1380 | 1 ⊢ (𝜑 → 𝜎) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ 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 395 df-3an 1087 |
This theorem is referenced by: dvfsumlem2 25779 noinfbnd2 27470 gg-dvfsumlem2 35469 atbtwnexOLDN 38621 atbtwnex 38622 osumcllem7N 39136 lhpmcvr5N 39201 cdleme22f2 39521 cdlemefs32sn1aw 39588 cdlemg7aN 39799 cdlemg7N 39800 cdlemg8c 39803 cdlemg8 39805 cdlemg11aq 39812 cdlemg12b 39818 cdlemg12e 39821 cdlemg12g 39823 cdlemg13a 39825 cdlemg15a 39829 cdlemg17e 39839 cdlemg18d 39855 cdlemg19a 39857 cdlemg20 39859 cdlemg22 39861 cdlemg28a 39867 cdlemg29 39879 cdlemg44a 39905 cdlemk34 40084 cdlemn11pre 40384 dihord10 40397 dihord2pre 40399 dihmeetlem17N 40497 |
Copyright terms: Public domain | W3C validator |