Theorem pm3.14 755

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 901. The converse holds for decidable propositions, as seen at pm3.13dc 962. (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 109	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2	1	con3i 633	. 2 ⊢ (¬ 𝜑 → ¬ (𝜑 ∧ 𝜓))
3		simpr 110	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
4	3	con3i 633	. 2 ⊢ (¬ 𝜓 → ¬ (𝜑 ∧ 𝜓))
5	2, 4	jaoi 718	1 ⊢ ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑 ∧ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 710

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 615  ax-in2 616  ax-io 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm3.1  756  xoranor  1397  difindiss  3428  swrdnd  11120