Metamath Proof Explorer


Theorem ichim

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

Ref Expression
Assertion ichim a b φ a b ψ a b φ ψ

Proof

Step Hyp Ref Expression
1 ichn a b ψ a b ¬ ψ
2 ichan a b φ a b ¬ ψ a b φ ¬ ψ
3 1 2 sylan2b a b φ a b ψ a b φ ¬ ψ
4 ichn a b φ ¬ ψ a b ¬ φ ¬ ψ
5 3 4 sylib a b φ a b ψ a b ¬ φ ¬ ψ
6 iman φ ψ ¬ φ ¬ ψ
7 6 a1i φ ψ ¬ φ ¬ ψ
8 7 ichbidv a b φ ψ a b ¬ φ ¬ ψ
9 8 mptru a b φ ψ a b ¬ φ ¬ ψ
10 5 9 sylibr a b φ a b ψ a b φ ψ