![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl2imc | Structured version Visualization version GIF version |
Description: A commuted version of syl2im 40. Implication-only version of syl2anr 598. (Contributed by BJ, 20-Oct-2021.) |
Ref | Expression |
---|---|
syl2im.1 | ⊢ (𝜑 → 𝜓) |
syl2im.2 | ⊢ (𝜒 → 𝜃) |
syl2im.3 | ⊢ (𝜓 → (𝜃 → 𝜏)) |
Ref | Expression |
---|---|
syl2imc | ⊢ (𝜒 → (𝜑 → 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl2im.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | syl2im.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
3 | syl2im.3 | . . 3 ⊢ (𝜓 → (𝜃 → 𝜏)) | |
4 | 1, 2, 3 | syl2im 40 | . 2 ⊢ (𝜑 → (𝜒 → 𝜏)) |
5 | 4 | com12 32 | 1 ⊢ (𝜒 → (𝜑 → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 |
This theorem is referenced by: impbid21d 210 nanass 1509 triun 5236 mapfvd 8751 undifixp 8806 rankpwi 9693 rankelb 9694 2cshwcshw 14647 incexclem 15657 sumeven 16205 cygth 20907 cnpco 22546 txkgen 22931 reperflem 24109 lhop1lem 25305 ulmss 25684 2sqreultblem 26724 crctcshwlkn0lem4 28563 numclwwlk1lem2f1 29106 ontgval 34834 bj-dvelimdv1 35249 eel12131 42796 et-sqrtnegnre 44905 2ffzoeq 45351 iccpartgt 45410 bgoldbtbndlem3 45790 lincresunit3 46353 |
Copyright terms: Public domain | W3C validator |