Theorem axc16i
Inference with axc16 as its conclusion. (Contributed by NM,
20-May-2008.) (Proof modification is discouraged.) Usage of this
theorem is discouraged because it depends on [ax-13]. Use axc16
instead. (New usage is discouraged.)
Hypotheses
axc16i.1
\( \vdash x = z \rightarrow (\varphi \leftrightarrow \psi) \)
axc16i.2
\( \vdash \psi \rightarrow \forall x \, \psi \)
Conclusion
\( \vdash \forall x \, x = y' \rightarrow \varphi \rightarrow \forall x \, \varphi \)
Proof
l0
nfv
l1
nfv
ax7
l3
cbv3 l0 l1 _
\( \vdash \forall x \, x = y' \rightarrow \forall z \, z = y' \)
ax7
\( \vdash z = x \rightarrow z = y' \rightarrow x = y' \)
l5
spimvw _
\( \vdash \forall z \, z = y' \rightarrow x = y' \)
l6
equcomi
\( \vdash x = y' \rightarrow y' = x \)
l7
equcomi
\( \vdash z = y' \rightarrow y' = z \)
ax7
\( \vdash y' = z \rightarrow y' = x \rightarrow z = x \)
syl l7 _
\( \vdash z = y' \rightarrow y' = x \rightarrow z = x \)
syl5com l6 _
alimdv _
\( \vdash x = y' \rightarrow \forall z \, z = y' \rightarrow \forall z \, z = x \)
l12
mpcom l5 _
\( \vdash \forall z \, z = y' \rightarrow \forall z \, z = x \)
l13
equcomi
\( \vdash z = x \rightarrow x = z \)
alimi _
\( \vdash \forall z \, z = x \rightarrow \forall z \, x = z \)
l15
syl l12 _
\( \vdash \forall z \, z = y' \rightarrow \forall z \, x = z \)
axc16i.1
biimpcd _
l18
alimdv _
\( \vdash \varphi \rightarrow \forall z \, x = z \rightarrow \forall z \, \psi \)
axc16i.2
l20
nf5i _
l21
nfv
axc16i.1
biimprd _
\( \vdash x = z \rightarrow \psi \rightarrow \varphi \)
syl l13 _
cbv3 l20 l21 _
\( \vdash \forall z \, \psi \rightarrow \forall x \, \varphi \)
syl6com l18 _
\( \vdash \forall z \, x = z \rightarrow \varphi \rightarrow \forall x \, \varphi \)
3syl l3 l15 _