Theorem eueqd ≪ | index | src | ≫ 

theorem eueqd (_G: wff) {x: nat} (_p1 _p2: wff x):
  $ _G -> (_p1 <-> _p2) $ >
  $ _G -> (eu x _p1 <-> eu x _p2) $;
StepHypRefExpression
1 hyp _ph 
_G -> (_p1 <-> _p2)
2 biidd 
_G -> (x = y <-> x = y)
3 1, 2 bieqd 
_G -> (_p1 <-> x = y <-> (_p2 <-> x = y))
4 3 aleqd 
_G -> (A. x (_p1 <-> x = y) <-> A. x (_p2 <-> x = y))
5 4 exeqd 
_G -> (E. y A. x (_p1 <-> x = y) <-> E. y A. x (_p2 <-> x = y))
6 5 conv eu 
_G -> (eu x _p1 <-> eu x _p2)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen, ax_4, ax_5)