Metamath Proof Explorer


Theorem naecoms-o

Description: A commutation rule for distinct variable specifiers. Version of naecoms using ax-c11 . (Contributed by NM, 2-Jan-2002) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis nalequcoms-o.1
|- ( -. A. x x = y -> ph )
Assertion naecoms-o
|- ( -. A. y y = x -> ph )

Proof

Step Hyp Ref Expression
1 nalequcoms-o.1
 |-  ( -. A. x x = y -> ph )
2 aecom-o
 |-  ( A. x x = y -> A. y y = x )
3 2 1 nsyl4
 |-  ( -. ph -> A. y y = x )
4 3 con1i
 |-  ( -. A. y y = x -> ph )