theorem Ifeq1d (_G _p1 _p2: wff) (A B: set): $ _G -> (_p1 <-> _p2) $ > $ _G -> If _p1 A B == If _p2 A B $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp _h | _G -> (_p1 <-> _p2) |
|
2 | eqsidd | _G -> A == A |
|
3 | eqsidd | _G -> B == B |
|
4 | 1, 2, 3 | Ifeqd | _G -> If _p1 A B == If _p2 A B |