theorem eqfal (a: wff): $ a <-> F. <-> ~a $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bitr | (a <-> F. <-> a -> F.) -> (a -> F. <-> ~a) -> (a <-> F. <-> ~a) |
|
| 2 | bian2 | (F. -> a) -> ((a -> F.) /\ (F. -> a) <-> a -> F.) |
|
| 3 | 2 | conv iff | (F. -> a) -> (a <-> F. <-> a -> F.) |
| 4 | efal | F. -> a |
|
| 5 | 3, 4 | ax_mp | a <-> F. <-> a -> F. |
| 6 | 1, 5 | ax_mp | (a -> F. <-> ~a) -> (a <-> F. <-> ~a) |
| 7 | imfal | a -> F. <-> ~a |
|
| 8 | 6, 7 | ax_mp | a <-> F. <-> ~a |