Theorem dfandc 892

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 642. (Contributed by Jim Kingdon, 30-Apr-2018.)

Assertion

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

Proof of Theorem dfandc

Step	Hyp	Ref	Expression
1		pm3.2im 642	. . . 4 ⊢ (𝜑 → (𝜓 → ¬ (𝜑 → ¬ 𝜓)))
2	1	imp 124	. . 3 ⊢ ((𝜑 ∧ 𝜓) → ¬ (𝜑 → ¬ 𝜓))
3		simplimdc 868	. . . . . . 7 ⊢ (DECID 𝜑 → (¬ (𝜑 → ¬ 𝜓) → 𝜑))
4	3	adantr 276	. . . . . 6 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → 𝜑))
5	4	imp 124	. . . . 5 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → 𝜑)
6		simprimdc 867	. . . . . . 7 ⊢ (DECID 𝜓 → (¬ (𝜑 → ¬ 𝜓) → 𝜓))
7	6	adantl 277	. . . . . 6 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → 𝜓))
8	7	imp 124	. . . . 5 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → 𝜓)
9	5, 8	jca 306	. . . 4 ⊢ (((DECID 𝜑 ∧ DECID 𝜓) ∧ ¬ (𝜑 → ¬ 𝜓)) → (𝜑 ∧ 𝜓))
10	9	ex 115	. . 3 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → (¬ (𝜑 → ¬ 𝜓) → (𝜑 ∧ 𝜓)))
11	2, 10	impbid2 143	. 2 ⊢ ((DECID 𝜑 ∧ DECID 𝜓) → ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓)))
12	11	ex 115	1 ⊢ (DECID 𝜑 → (DECID 𝜓 → ((𝜑 ∧ 𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717

This theorem depends on definitions:  df-bi 117  df-stab 839  df-dc 843

This theorem is referenced by:  pm4.63dc  894  pm4.54dc  910