theorem com12b (a b c: wff): $ a -> b -> c <-> b -> a -> c $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id | (a -> b -> c) -> a -> b -> c |
|
2 | 1 | com23 | (a -> b -> c) -> b -> a -> c |
3 | id | (b -> a -> c) -> b -> a -> c |
|
4 | 3 | com23 | (b -> a -> c) -> a -> b -> c |
5 | 2, 4 | ibii | a -> b -> c <-> b -> a -> c |