theorem booleqd (_G: wff) (_n1 _n2: nat): $ _G -> _n1 = _n2 $ > $ _G -> (bool _n1 <-> bool _n2) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp _nh | _G -> _n1 = _n2 |
|
2 | eqidd | _G -> 2 = 2 |
|
3 | 1, 2 | lteqd | _G -> (_n1 < 2 <-> _n2 < 2) |
4 | 3 | conv bool | _G -> (bool _n1 <-> bool _n2) |