Description: Derive ax-c15 from a hypothesis in the form of ax-12 , without using
ax-12 or ax-c15 . The hypothesis is weaker than ax-12 , with
z both distinct from x and not occurring in ph . Thus, the
hypothesis provides an alternate axiom that can be used in place of
ax-12 , if we also have ax-c11 , which this proof uses. As Theorem
ax12 shows, the distinct variable conditions are optional. An open
problem is whether we can derive this with ax-c11n instead of
ax-c11 . (Contributed by NM, 2-Feb-2007)(Proof modification is discouraged.)(New usage is discouraged.)
Ref
Expression
Hypothesis
ax12a2-o.1
|- ( x = z -> ( A. z ph -> A. x ( x = z -> ph ) ) )