Theorem dfandc 822

Description: Definition of 'and' in terms of negation and implication, for decidable propositions. The forward direction holds for all propositions, and can (basically) be found at pm3.2im 606. (Contributed by Jim Kingdon, 30-Apr-2018.)

Assertion

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

Proof of Theorem dfandc

Step	Hyp	Ref	Expression
1		pm3.2im 606	. . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
2	1	imp 123	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓))
3		simplimdc 801	. . . . . . 7 ⊢ (DECID 𝜑 → (¬ (𝜑 → ¬ 𝜓) → 𝜑))
4	3	adantr 272	. . . . . 6 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → 𝜑))
5	4	imp 123	. . . . 5 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → 𝜑)
6		simprimdc 800	. . . . . . 7 ⊢ (DECID 𝜓 → (¬ (𝜑 → ¬ 𝜓) → 𝜓))
7	6	adantl 273	. . . . . 6 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → 𝜓))
8	7	imp 123	. . . . 5 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → 𝜓)
9	5, 8	jca 302	. . . 4 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → (𝜑 ∧ 𝜓))
10	9	ex 114	. . 3 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → (𝜑 ∧ 𝜓)))
11	2, 10	impbid2 142	. 2 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)))
12	11	ex 114	1 ⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))))

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

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 584  ax-in2 585  ax-io 671

This theorem depends on definitions:  df-bi 116  df-dc 787

This theorem is referenced by:  pm4.63dc  824  pm4.54dc  849