Theorem ifpeq | index | src |

theorem ifpeq (_p1 _p2 _a1 _a2 _b1 _b2: wff):
  $ (_p1 <-> _p2) ->
    (_a1 <-> _a2) ->
    (_b1 <-> _b2) ->
    (ifp _p1 _a1 _b1 <-> ifp _p2 _a2 _b2) $;
StepHypRefExpression
1 anl
(_p1 <-> _p2) /\ (_a1 <-> _a2) -> (_p1 <-> _p2)
2 1 anwl
(_p1 <-> _p2) /\ (_a1 <-> _a2) /\ (_b1 <-> _b2) -> (_p1 <-> _p2)
3 anr
(_p1 <-> _p2) /\ (_a1 <-> _a2) -> (_a1 <-> _a2)
4 3 anwl
(_p1 <-> _p2) /\ (_a1 <-> _a2) /\ (_b1 <-> _b2) -> (_a1 <-> _a2)
5 anr
(_p1 <-> _p2) /\ (_a1 <-> _a2) /\ (_b1 <-> _b2) -> (_b1 <-> _b2)
6 2, 4, 5 ifpeqd
(_p1 <-> _p2) /\ (_a1 <-> _a2) /\ (_b1 <-> _b2) -> (ifp _p1 _a1 _b1 <-> ifp _p2 _a2 _b2)
7 6 exp
(_p1 <-> _p2) /\ (_a1 <-> _a2) -> (_b1 <-> _b2) -> (ifp _p1 _a1 _b1 <-> ifp _p2 _a2 _b2)
8 7 exp
(_p1 <-> _p2) -> (_a1 <-> _a2) -> (_b1 <-> _b2) -> (ifp _p1 _a1 _b1 <-> ifp _p2 _a2 _b2)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)