Theorem annimdc 881

Description: Express conjunction in terms of implication. The forward direction, annimim 818, is valid for all propositions, but as an equivalence, it requires a decidability condition. (Contributed by Jim Kingdon, 25-Apr-2018.)

Assertion

Ref	Expression
annimdc	⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))))

Proof of Theorem annimdc

Step	Hyp	Ref	Expression
1		imandc 822	. . . 4 ⊢ (DECID 𝜓 → ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)))
2	1	adantl 271	. . 3 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)))
3		dcim 820	. . . . 5 ⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 → 𝜓)))
4	3	imp 122	. . . 4 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → DECID (𝜑 → 𝜓))
5		dcn 782	. . . . . 6 ⊢ (DECID 𝜓 → DECID ¬ 𝜓)
6		dcan 878	. . . . . 6 ⊢ (DECID 𝜑 → (DECID ¬ 𝜓 → DECID (𝜑 ∧ ¬ 𝜓)))
7	5, 6	syl5 32	. . . . 5 ⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∧ ¬ 𝜓)))
8	7	imp 122	. . . 4 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → DECID (𝜑 ∧ ¬ 𝜓))
9		con2bidc 805	. . . 4 ⊢ (DECID (𝜑 → 𝜓) → (DECID (𝜑 ∧ ¬ 𝜓) → (((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) ↔ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)))))
10	4, 8, 9	sylc 61	. . 3 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → (((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) ↔ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))))
11	2, 10	mpbid 145	. 2 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)))
12	11	ex 113	1 ⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 102   ↔ wb 103  DECID wdc 778

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663

This theorem depends on definitions:  df-bi 115  df-dc 779

This theorem is referenced by:  xordidc  1333