Metamath Proof Explorer


Theorem snexOLD

Description: Obsolete version of snex as of 6-Mar-2026. (Contributed by NM, 7-Aug-1994) (Revised by Mario Carneiro, 19-May-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion snexOLD A V

Proof

Step Hyp Ref Expression
1 snexg A V A V
2 snprc ¬ A V A =
3 2 biimpi ¬ A V A =
4 0ex V
5 3 4 eqeltrdi ¬ A V A V
6 1 5 pm2.61i A V