Metamath Proof Explorer


Theorem bj-andnotim

Description: Two ways of expressing a certain ternary connective. Note the respective positions of the three formulas on each side of the biconditional. (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-andnotim ( ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝜒 ) ↔ ( ( 𝜑𝜓 ) ∨ 𝜒 ) )

Proof

Step Hyp Ref Expression
1 imor ( ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝜒 ) ↔ ( ¬ ( 𝜑 ∧ ¬ 𝜓 ) ∨ 𝜒 ) )
2 iman ( ( 𝜑𝜓 ) ↔ ¬ ( 𝜑 ∧ ¬ 𝜓 ) )
3 2 biimpri ( ¬ ( 𝜑 ∧ ¬ 𝜓 ) → ( 𝜑𝜓 ) )
4 3 orim1i ( ( ¬ ( 𝜑 ∧ ¬ 𝜓 ) ∨ 𝜒 ) → ( ( 𝜑𝜓 ) ∨ 𝜒 ) )
5 1 4 sylbi ( ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝜒 ) → ( ( 𝜑𝜓 ) ∨ 𝜒 ) )
6 pm2.24 ( 𝜓 → ( ¬ 𝜓𝜒 ) )
7 6 imim2i ( ( 𝜑𝜓 ) → ( 𝜑 → ( ¬ 𝜓𝜒 ) ) )
8 7 impd ( ( 𝜑𝜓 ) → ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝜒 ) )
9 ax-1 ( 𝜒 → ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝜒 ) )
10 8 9 jaoi ( ( ( 𝜑𝜓 ) ∨ 𝜒 ) → ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝜒 ) )
11 5 10 impbii ( ( ( 𝜑 ∧ ¬ 𝜓 ) → 𝜒 ) ↔ ( ( 𝜑𝜓 ) ∨ 𝜒 ) )