![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl311anc | 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 | ⊢ (𝜑 → 𝜂) |
syl311anc.6 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁) |
Ref | Expression |
---|---|
syl311anc | ⊢ (𝜑 → 𝜁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl3anc.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | syl3anc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | syl3anc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | 1, 2, 3 | 3jca 1119 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
5 | syl3Xanc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl311anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁) | |
8 | 4, 5, 6, 7 | syl3anc 1439 | 1 ⊢ (𝜑 → 𝜁) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1071 |
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 199 df-an 387 df-3an 1073 |
This theorem is referenced by: syl312anc 1459 syl321anc 1460 syl313anc 1462 syl331anc 1463 pythagtrip 15943 nmolb2d 22930 nmoleub 22943 clwwisshclwwslem 27403 numclwwlk1lem2foa 27783 numclwwlk1lem2foaOLD 27784 cvlcvr1 35487 4atlem12b 35759 dalawlem10 36028 dalawlem13 36031 dalawlem15 36033 osumcllem11N 36114 lhp2atne 36182 lhp2at0ne 36184 cdlemd 36355 ltrneq3 36356 cdleme7d 36394 cdlemeg49le 36659 cdleme 36708 cdlemg1a 36718 ltrniotavalbN 36732 cdlemg44 36881 cdlemk19 37017 cdlemk27-3 37055 cdlemk33N 37057 cdlemk34 37058 cdlemk49 37099 cdlemk53a 37103 cdlemk19u 37118 cdlemk56w 37121 dia2dimlem4 37215 dih1dimatlem0 37476 itsclc0yqe 43489 itsclinecirc0 43501 itsclinecirc0b 43502 inlinecirc02plem 43514 |
Copyright terms: Public domain | W3C validator |