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.)