Metamath Proof Explorer


Theorem ax6er

Description: Commuted form of ax6e . (Could be placed right after ax6e ). (Contributed by BJ, 15-Sep-2018)

Ref Expression
Assertion ax6er 𝑥 𝑦 = 𝑥

Proof

Step Hyp Ref Expression
1 ax6e 𝑥 𝑥 = 𝑦
2 equcomi ( 𝑥 = 𝑦𝑦 = 𝑥 )
3 1 2 eximii 𝑥 𝑦 = 𝑥