Implication elimination: A → B = NOT A OR B, and the →E rule
Implication elimination rewrites A -> B as NOT A OR B: an implication is true unless its condition holds and its consequence fails. In natural deduction the same name means the inference rule →E, modus ponens: from A -> B and A, infer B.
An implication is rewritten as the negated condition OR the consequence.
The truth table of implication surprises people the first time: A -> B is true whenever A is false, whatever B is. The identity makes that visible. NOT A OR B is false only on the row A = TRUE, B = FALSE, which is the one case where a promise “if A then B” is broken. Every other row keeps the promise, including the rows where A never happened.
The normal-form converter and the NAND-only and NOR-only constructions apply this law first, because they work with AND, OR and NOT only. The simplifier keeps the arrow and has its own rules for an implication with a constant, equal or complementary operands: A -> TRUE folds to TRUE by domination. It is also the law behind the contrapositive, since NOT B -> NOT A eliminates to B OR NOT A, the same formula with its operands swapped.
The four-row proof is below. The operator page on implication explains the reading, and the pitfalls on the converse and on necessary versus sufficient conditions show what the law does not license.
Statement
A -> B = NOT A OR B Proof by truth table: A -> B = NOT A OR B
| # | A | B | lhs | rhs |
|---|---|---|---|---|
| 0 | FALSE | FALSE | TRUE | TRUE |
| 1 | FALSE | TRUE | TRUE | TRUE |
| 2 | TRUE | FALSE | FALSE | FALSE |
| 3 | TRUE | TRUE | TRUE | TRUE |
The same law in four notations
A -> BA -> BA → BA → BA \rightarrow BNOT A OR B!A || B¬A ∨ BA' + B\overline{A} + BImplication elimination in natural deduction (→E)
In a natural-deduction proof, implication elimination (→E, also called conditional elimination) is a rule of inference rather than a rewrite: from a line A -> B and a line A, you may write B. It is the rule known as modus ponens. Its argument form, premises A -> B and A with conclusion B, is valid: no row of its truth table makes both premises TRUE and B FALSE, and the modus ponens worked example checks exactly that.
The rewrite on this page explains why the rule is safe. A -> B is the same as NOT A OR B, so once A is TRUE the only way left for the implication to hold is for B to be TRUE. Tangibool checks arguments by truth table; it does not build natural-deduction proofs line by line.
The common slip
Rewriting A -> B as A AND B or as B -> A. The first makes the implication false when A is false; the second is the converse, a different claim. Only NOT A OR B is equivalent.
Questions
How do I write “A only if B”?
As A -> B. “Only if” names the necessary condition: A can hold only when B does. “A if B” is B -> A. The lesson on necessary and sufficient conditions drills the difference.
Is implication elimination the same as modus ponens?
In natural deduction, yes: the rule →E is modus ponens. In Boolean algebra the same name means the rewrite of A -> B as NOT A OR B, which this page proves by truth table.
Related
Lesson that teaches this
Tools
- Boolean algebra calculator and simplifier with steps (every law named and verified)
- Logical equivalence checker: two expressions, exact verdict, counterexample
Practice
See also
- Modus ponens: A → B, A, therefore B (valid)
- Implication (→, if–then): truth table and why a false antecedent makes it true
- Implication as NOT A OR B, verified
- Contrapositive: A → B is equivalent to NOT B → NOT A
- A → B does not give B → A
- Necessary vs sufficient: “only if” is not “if”
- Lesson 5: If, only if, unless: necessary and sufficient conditions (intermediate, 15 min)
Laws
Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build . Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.