![]() |
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 53 | 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 91 bi3ant 213 pm3.41 314 pm3.42 315 jarl 583 pm2.67-2 633 oibabs 799 pm2.85dc 810 peircedc 819 3jaob 1196 hbim 1434 hbimd 1462 i19.39 1528 hbae 1603 sbcof2 1688 sb4or 1711 tfi 4248 dmcosseq 4546 fliftfun 5379 setindis 9427 bdsetindis 9429 |
Copyright terms: Public domain | W3C validator |