Theorem ax13b

An equivalence between two ways of expressing [ax-13]. See the comment for [ax-13]. (Contributed by NM, 2-May-2017.) (Proof shortened by Wolf Lammen, 26-Feb-2018.) (Revised by BJ, 15-Sep-2020.)

Conclusion
\( \vdash \neg x' = y' \rightarrow y' = z' \rightarrow \varphi \leftrightarrow \neg x' = y' \rightarrow \neg x' = z' \rightarrow y' = z' \rightarrow \varphi \)
Proof
l0
ax-1
equeuclr
con3rr3 _
l3
imim1d _
\( \vdash \neg x' = y' \rightarrow (\neg x' = z' \rightarrow y' = z' \rightarrow \varphi) \rightarrow y' = z' \rightarrow y' = z' \rightarrow \varphi \)
pm2.43
\( \vdash (y' = z' \rightarrow y' = z' \rightarrow \varphi) \rightarrow y' = z' \rightarrow \varphi \)
syl6 l3 _
impbid2 l0 _
pm5.74i _