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 512 | . 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 1374 | 1 ⊢ (𝜑 → 𝜎) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: dvfsumlem2 24551 atbtwnexOLDN 36463 atbtwnex 36464 osumcllem7N 36978 lhpmcvr5N 37043 cdleme22f2 37363 cdlemefs32sn1aw 37430 cdlemg7aN 37641 cdlemg7N 37642 cdlemg8c 37645 cdlemg8 37647 cdlemg11aq 37654 cdlemg12b 37660 cdlemg12e 37663 cdlemg12g 37665 cdlemg13a 37667 cdlemg15a 37671 cdlemg17e 37681 cdlemg18d 37697 cdlemg19a 37699 cdlemg20 37701 cdlemg22 37703 cdlemg28a 37709 cdlemg29 37721 cdlemg44a 37747 cdlemk34 37926 cdlemn11pre 38226 dihord10 38239 dihord2pre 38241 dihmeetlem17N 38339 |
Copyright terms: Public domain | W3C validator |