Description: Weak version of excomim . Uses only Tarski's FOL axiom schemes. (Contributed by BTernaryTau, 23-Jun-2025)
Ref | Expression | ||
---|---|---|---|
Hypothesis | excomimw.1 | ||
Assertion | excomimw |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | excomimw.1 | ||
2 | 1 | notbid | |
3 | 2 | alcomimw | |
4 | 3 | con3i | |
5 | 2exnaln | ||
6 | 2exnaln | ||
7 | 4 5 6 | 3imtr4i |