Metamath Proof Explorer


Theorem icht

Description: A theorem is interchangeable. (Contributed by SN, 4-May-2024)

Ref Expression
Hypothesis icht.1 φ
Assertion icht x y φ

Proof

Step Hyp Ref Expression
1 icht.1 φ
2 1 sbt a y φ
3 2 sbt y x a y φ
4 3 sbt x a y x a y φ
5 4 1 2th x a y x a y φ φ
6 5 gen2 x y x a y x a y φ φ
7 df-ich x y φ x y x a y x a y φ φ
8 6 7 mpbir x y φ