Skip to content

Commit

Permalink
doc: add omitted word
Browse files Browse the repository at this point in the history
  • Loading branch information
chabulhwi committed Sep 30, 2024
1 parent 9782b5c commit 2884512
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion docs/en/notes/chapter03/propositional-connectives.md
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@
* Meaning: given `p q : Prop`, the proposition `p ↔ q` stands for "`p` if and
only if `q`" (often abbreviated as "`p` iff `q`").
* Rules of inference
- Introduction rule: `p ↔ q` follows `p → q` and `q → p`. (`Iff.intro`)
- Introduction rule: `p ↔ q` follows from `p → q` and `q → p`. (`Iff.intro`)
- Elimination rules
+ `p → q` follows from `p ↔ q`. (`Iff.mp`, modus ponens for iff)
+ `q → p` follows from `p ↔ q`. (`Iff.mpr`, reversed modus ponens for iff)

0 comments on commit 2884512

Please sign in to comment.