Description: Biconditional of its own negation is a contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | bicontr | ⊢ ( ( ¬ 𝜑 ↔ 𝜑 ) ↔ ⊥ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biid | ⊢ ( 𝜑 ↔ 𝜑 ) | |
2 | notbinot1 | ⊢ ( ¬ ( ¬ 𝜑 ↔ 𝜑 ) ↔ ( 𝜑 ↔ 𝜑 ) ) | |
3 | 1 2 | mpbir | ⊢ ¬ ( ¬ 𝜑 ↔ 𝜑 ) |
4 | 3 | bifal | ⊢ ( ( ¬ 𝜑 ↔ 𝜑 ) ↔ ⊥ ) |