Metamath Proof Explorer


Theorem ichbidv

Description: Formula building rule for interchangeability (deduction). (Contributed by SN, 4-May-2024)

Ref Expression
Hypothesis ichbidv.1 φ ψ χ
Assertion ichbidv φ x y ψ x y χ

Proof

Step Hyp Ref Expression
1 ichbidv.1 φ ψ χ
2 1 sbbidv φ a y ψ a y χ
3 2 sbbidv φ y x a y ψ y x a y χ
4 3 sbbidv φ x a y x a y ψ x a y x a y χ
5 4 1 bibi12d φ x a y x a y ψ ψ x a y x a y χ χ
6 5 albidv φ y x a y x a y ψ ψ y x a y x a y χ χ
7 6 albidv φ x y x a y x a y ψ ψ x y x a y x a y χ χ
8 df-ich x y ψ x y x a y x a y ψ ψ
9 df-ich x y χ x y x a y x a y χ χ
10 7 8 9 3bitr4g φ x y ψ x y χ