Theorem pm3.14 748

Description: Theorem *3.14 of [WhiteheadRussell] p. 111. One direction of De Morgan's law). The biconditional holds for decidable propositions as seen at ianordc 894. The converse holds for decidable propositions, as seen at pm3.13dc 954. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)

Assertion

Ref	Expression
pm3.14	⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))

Proof of Theorem pm3.14

Step	Hyp	Ref	Expression
1		simpl 108	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	con3i 627	. 2 ⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓))
3		simpr 109	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	con3i 627	. 2 ⊢ (¬ 𝜓 → ¬ (𝜑 ∧ 𝜓))
5	2, 4	jaoi 711	1 ⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ∨ wo 703

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 609  ax-in2 610  ax-io 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm3.1  749  xoranor  1372  difindiss  3381