Theorem annimdc 902

Description: Express conjunction in terms of implication. The forward direction, annimim 658, 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 855	. . . 4 ⊢ (DECID 𝜓 → ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)))
2	1	adantl 273	. . 3 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)))
3		dcim 809	. . . . 5 ⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 → 𝜓)))
4	3	imp 123	. . . 4 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → DECID (𝜑 → 𝜓))
5		dcn 810	. . . . . 6 ⊢ (DECID 𝜓 → DECID ¬ 𝜓)
6		dcan 899	. . . . . 6 ⊢ (DECID 𝜑 → (DECID ¬ 𝜓 → DECID (𝜑 ∧ ¬ 𝜓)))
7	5, 6	syl5 32	. . . . 5 ⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∧ ¬ 𝜓)))
8	7	imp 123	. . . 4 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → DECID (𝜑 ∧ ¬ 𝜓))
9		con2bidc 841	. . . 4 ⊢ (DECID (𝜑 → 𝜓) → (DECID (𝜑 ∧ ¬ 𝜓) → (((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) ↔ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)))))
10	4, 8, 9	sylc 62	. . 3 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → (((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)) ↔ ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))))
11	2, 10	mpbid 146	. 2 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓)))
12	11	ex 114	1 ⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ ¬ 𝜓) ↔ ¬ (𝜑 → 𝜓))))

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681

This theorem depends on definitions:  df-bi 116  df-stab 799  df-dc 803

This theorem is referenced by:  xordidc  1358