![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > imim1i | GIF version |
Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.) |
Ref | Expression |
---|---|
imim1i.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
imim1i | ⊢ ((𝜓 → 𝜒) → (𝜑 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imim1i.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | id 19 | . 2 ⊢ (𝜒 → 𝜒) | |
3 | 1, 2 | imim12i 58 | 1 ⊢ ((𝜓 → 𝜒) → (𝜑 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 |
This theorem is referenced by: jarr 96 bi3ant 222 pm3.41 324 pm3.42 325 jarl 619 pm2.67-2 669 oibabs 838 pm2.85dc 849 peircedc 858 3jaob 1238 hbim 1482 hbimd 1510 i19.39 1576 hbae 1653 sbcof2 1738 sb4or 1761 tfi 4397 dmcosseq 4704 fliftfun 5575 tfrcl 6129 ac6sfi 6614 fsum2d 10829 fsumabs 10859 fsumiun 10871 setindis 11862 bdsetindis 11864 |
Copyright terms: Public domain | W3C validator |