![]() |
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 |
---|---|
syl12anc.1 | ⊢ (𝜑 → 𝜓) |
syl12anc.2 | ⊢ (𝜑 → 𝜒) |
syl12anc.3 | ⊢ (𝜑 → 𝜃) |
syl22anc.4 | ⊢ (𝜑 → 𝜏) |
syl23anc.5 | ⊢ (𝜑 → 𝜂) |
syl311anc.6 | ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁) |
Ref | Expression |
---|---|
syl311anc | ⊢ (𝜑 → 𝜁) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl12anc.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | syl12anc.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | syl12anc.3 | . . 3 ⊢ (𝜑 → 𝜃) | |
4 | 1, 2, 3 | 3jca 1122 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒 ∧ 𝜃)) |
5 | syl22anc.4 | . 2 ⊢ (𝜑 → 𝜏) | |
6 | syl23anc.5 | . 2 ⊢ (𝜑 → 𝜂) | |
7 | syl311anc.6 | . 2 ⊢ (((𝜓 ∧ 𝜒 ∧ 𝜃) ∧ 𝜏 ∧ 𝜂) → 𝜁) | |
8 | 4, 5, 6, 7 | syl3anc 1476 | 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 197 df-an 383 df-3an 1073 |
This theorem is referenced by: syl312anc 1497 syl321anc 1498 syl313anc 1500 syl331anc 1501 pythagtrip 15746 nmolb2d 22742 nmoleub 22755 clwwisshclwwslem 27164 numclwwlk1lem2foa 27540 cvlcvr1 35148 4atlem12b 35419 dalawlem10 35688 dalawlem13 35691 dalawlem15 35693 osumcllem11N 35774 lhp2atne 35842 lhp2at0ne 35844 cdlemd 36016 ltrneq3 36017 cdleme7d 36055 cdlemeg49le 36320 cdleme 36369 cdlemg1a 36379 ltrniotavalbN 36393 cdlemg44 36542 cdlemk19 36678 cdlemk27-3 36716 cdlemk33N 36718 cdlemk34 36719 cdlemk49 36760 cdlemk53a 36764 cdlemk19u 36779 cdlemk56w 36782 dia2dimlem4 36877 dih1dimatlem0 37138 |
Copyright terms: Public domain | W3C validator |