Theorem annimdc 927

Description: Express conjunction in terms of implication. The forward direction, annimim 676, 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 879	. . . 4 ⊢ (DECID 𝜓 → ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)))
2	1	adantl 275	. . 3 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → ((𝜑 → 𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)))
3		dcim 831	. . . . 5 ⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 → 𝜓)))
4	3	imp 123	. . . 4 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → DECID (𝜑 → 𝜓))
5		dcn 832	. . . . . 6 ⊢ (DECID 𝜓 → DECID ¬ 𝜓)
6		dcan2 924	. . . . . 6 ⊢ (DECID 𝜑 → (DECID ¬ 𝜓 → DECID (𝜑 ∧ ¬ 𝜓)))
7	5, 6	syl5 32	. . . . 5 ⊢ (DECID 𝜑 → (DECID 𝜓 → DECID (𝜑 ∧ ¬ 𝜓)))
8	7	imp 123	. . . 4 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → DECID (𝜑 ∧ ¬ 𝜓))
9		con2bidc 865	. . . 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 824

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

This theorem depends on definitions:  df-bi 116  df-stab 821  df-dc 825

This theorem is referenced by:  xordidc  1389