Expand description
Tactics for Logical IMPLY.
Functions
false => a
.
((a ∧ b) => c => a => (b => c))
.
(a => b) => ¬¬a => ¬¬b
.
(¬a => b) => (¬b => a)
.
(a => ¬b) => (b => ¬a)
.
(¬a ∨ b) => (a => b)
.
a => a
.
(a => b) ∧ (a = c) => (c => b)
.
(a => b) ∧ (b = c) => (a => c)
.
(a => c) ∧ (b => c) => ((a ∧ b) => c)
.
(a => b) ∧ a => b
a => b => ¬b => ¬a
.
a => (b => c) => b => (a => c)
(¬¬a => ¬¬b) => a => b
.
(b => a) ∧ ¬a => ¬b
.
¬b => ¬a => a => b
.
(a => b) => (¬a ∨ b)
.
a => b ∧ b => c => a => c
.