![]() |
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 5241 mapfvd 8823 undifixp 8878 rankpwi 9767 rankelb 9768 2cshwcshw 14723 incexclem 15729 sumeven 16277 cygth 21001 cnpco 22641 txkgen 23026 reperflem 24204 lhop1lem 25400 ulmss 25779 2sqreultblem 26819 crctcshwlkn0lem4 28807 numclwwlk1lem2f1 29350 ontgval 34956 bj-dvelimdv1 35371 eel12131 43087 et-sqrtnegnre 45204 2ffzoeq 45650 iccpartgt 45709 bgoldbtbndlem3 46089 lincresunit3 46652 |
Copyright terms: Public domain | W3C validator |