Metamath Proof Explorer


Theorem excomimw

Description: Weak version of excomim . Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 23-Jun-2025)

Ref Expression
Hypothesis excomimw.1 x = z φ ψ
Assertion excomimw x y φ y x φ

Proof

Step Hyp Ref Expression
1 excomimw.1 x = z φ ψ
2 1 notbid x = z ¬ φ ¬ ψ
3 2 alcomimw y x ¬ φ x y ¬ φ
4 3 con3i ¬ x y ¬ φ ¬ y x ¬ φ
5 2exnaln x y φ ¬ x y ¬ φ
6 2exnaln y x φ ¬ y x ¬ φ
7 4 5 6 3imtr4i x y φ y x φ