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