Theorem pm11.07 2089

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

Hypothesis

Ref	Expression
pm11.07.1	⊢ 𝜑

Assertion

Ref	Expression
pm11.07	⊢ 𝜑

Proof of Theorem pm11.07

Step	Hyp	Ref	Expression
1		pm11.07.1	1 ⊢ 𝜑

This theorem is referenced by: (None)