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	⊢ ( ( [ 𝑎 ⇄ 𝑏 ] 𝜑 ∧ [ 𝑎 ⇄ 𝑏 ] 𝜓 ) → [ 𝑎 ⇄ 𝑏 ] ( 𝜑 → 𝜓 ) )