Metamath Proof Explorer

Theorem ich2al

Description: Two setvar variables are always interchangeable when there are two universal quantifiers. (Contributed by SN, 23-Nov-2023)

Ref Expression
Assertion ich2al 
|- [ x <> y ] A. x A. y ph

Proof

Step Hyp Ref Expression
1 nfa1 
 |-  F/ x A. x A. y ph
2 nfa2 
 |-  F/ y A. x A. y ph
3 1 2 ichf 
 |-  [ x <> y ] A. x A. y ph