theorem nateqd (_G _p1 _p2: wff): $ _G -> (_p1 <-> _p2) $ > $ _G -> nat _p1 = nat _p2 $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp _ph | _G -> (_p1 <-> _p2) |
|
2 | eqidd | _G -> 1 = 1 |
|
3 | eqidd | _G -> 0 = 0 |
|
4 | 1, 2, 3 | ifeqd | _G -> if _p1 1 0 = if _p2 1 0 |
5 | 4 | conv nat | _G -> nat _p1 = nat _p2 |