Theorem bijust 145

Description: Theorem used to justify definition of biconditional df-bi 147. (The proof was shortened by Josh Purinton, 29-Dec-00.)

Assertion

Ref	Expression
bijust	⊢ ¬ ((φ → φ) → ¬ (φ → φ))

Proof of Theorem bijust

Step	Hyp	Ref	Expression
1		id 59	. 2 ⊢ (φ → φ)
2		pm2.01 88	. 2 ⊢ (((φ → φ) → ¬ (φ → φ)) → ¬ (φ → φ))
3	1, 2	mt2 109	1 ⊢ ¬ ((φ → φ) → ¬ (φ → φ))

Syntax hints:  ¬ wn 2   → wi 3

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

Copyright terms: Public domain