Metamath Proof Explorer


Theorem axreplem

Description: Lemma for axrep2 and axrep3 . (Contributed by BJ, 6-Aug-2022)

Ref Expression
Assertion axreplem x = y u φ v ψ w z x χ u φ v ψ w z y χ

Proof

Step Hyp Ref Expression
1 elequ2 x = y z x z y
2 1 anbi1d x = y z x χ z y χ
3 2 exbidv x = y w z x χ w z y χ
4 3 bibi2d x = y ψ w z x χ ψ w z y χ
5 4 albidv x = y v ψ w z x χ v ψ w z y χ
6 5 imbi2d x = y φ v ψ w z x χ φ v ψ w z y χ
7 6 exbidv x = y u φ v ψ w z x χ u φ v ψ w z y χ