Description: Axiom *11.07 in WhiteheadRussell p. 159. The original reads: *11.07
"Whatever possible argument x may be, ph ( x , y ) is true
whatever possible argument y may be" implies the corresponding
statement with x and y interchanged except
in " ph ( x , y ) ". Under our formalism this appears to correspond
to idi and not to sbcom4 as earlier thought. See
https://groups.google.com/g/metamath/c/iS0fOvSemC8/m/M1zTH8wxCAAJ .
(Contributed by BJ, 16-Sep-2018)(New usage is discouraged.)