Description: Version of axc10 with a disjoint variable condition, which does not require ax-13 . (Contributed by BJ, 14-Jun-2019) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-axc10v |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax6v | ||
2 | con3 | ||
3 | 2 | al2imi | |
4 | 1 3 | mtoi | |
5 | axc7 | ||
6 | 4 5 | syl |