Biconditional with Factor of Biconditional
Jump to navigation
Jump to search
Theorem
- $\paren {p \iff q} \iff q \dashv \vdash p$
Proof
| \(\ds \paren {p \iff q} \iff q\) | \(\dashv \vdash\) | \(\ds p \iff \paren {q \iff q}\) | Biconditional is Associative | |||||||||||
| \(\ds \) | \(\dashv \vdash\) | \(\ds p \iff \top\) | Biconditional with Itself | |||||||||||
| \(\ds \) | \(\dashv \vdash\) | \(\ds p\) | Biconditional with Tautology |
$\blacksquare$
Sources
- 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.10$: Exercise $2.4$