This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ichim

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

Ref Expression
Assertion ichim ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜓 ) → [ 𝑎 ⇄ 𝑏 ] ( 𝜑 → 𝜓 ) )

Proof

Step Hyp Ref Expression
1 ichn ⊢ ( [ 𝑎 ⇄ 𝑏 ] 𝜓 ↔ [ 𝑎 ⇄ 𝑏 ] ¬ 𝜓 )
2 ichan ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ [ 𝑎 ⇄ 𝑏 ] ¬ 𝜓 ) → [ 𝑎 ⇄ 𝑏 ] ( 𝜑 ∧ ¬ 𝜓 ) )
3 1 2 sylan2b ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜓 ) → [ 𝑎 ⇄ 𝑏 ] ( 𝜑 ∧ ¬ 𝜓 ) )
4 ichn ⊢ ( [ 𝑎 ⇄ 𝑏 ] ( 𝜑 ∧ ¬ 𝜓 ) ↔ [ 𝑎 ⇄ 𝑏 ] ¬ ( 𝜑 ∧ ¬ 𝜓 ) )
5 3 4 sylib ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜓 ) → [ 𝑎 ⇄ 𝑏 ] ¬ ( 𝜑 ∧ ¬ 𝜓 ) )
6 iman ⊢ ( ( 𝜑 → 𝜓 ) ↔ ¬ ( 𝜑 ∧ ¬ 𝜓 ) )
7 6 a1i ⊢ ( ⊤ → ( ( 𝜑 → 𝜓 ) ↔ ¬ ( 𝜑 ∧ ¬ 𝜓 ) ) )
8 7 ichbidv ⊢ ( ⊤ → ( [ 𝑎 ⇄ 𝑏 ] ( 𝜑 → 𝜓 ) ↔ [ 𝑎 ⇄ 𝑏 ] ¬ ( 𝜑 ∧ ¬ 𝜓 ) ) )
9 8 mptru ⊢ ( [ 𝑎 ⇄ 𝑏 ] ( 𝜑 → 𝜓 ) ↔ [ 𝑎 ⇄ 𝑏 ] ¬ ( 𝜑 ∧ ¬ 𝜓 ) )
10 5 9 sylibr ⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜓 ) → [ 𝑎 ⇄ 𝑏 ] ( 𝜑 → 𝜓 ) )