Metamath Proof Explorer
Description: Theorem used to justify the definition of the biconditional df-bi .
Instance of bijust0 . (Contributed by NM, 11-May-1999)
|
|
Ref |
Expression |
|
Assertion |
bijust |
⊢ ¬ ( ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
bijust0 |
⊢ ¬ ( ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) → ¬ ( ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) → ¬ ( ( 𝜑 → 𝜓 ) → ¬ ( 𝜓 → 𝜑 ) ) ) ) |