ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm3.14 GIF version

Theorem pm3.14 703
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 833. The converse holds for decidable propositions, as seen at pm3.13dc 901. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
Assertion
Ref Expression
pm3.14 ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑𝜓))

Proof of Theorem pm3.14
StepHypRef Expression
1 simpl 107 . . 3 ((𝜑𝜓) → 𝜑)
21con3i 595 . 2 𝜑 → ¬ (𝜑𝜓))
3 simpr 108 . . 3 ((𝜑𝜓) → 𝜓)
43con3i 595 . 2 𝜓 → ¬ (𝜑𝜓))
52, 4jaoi 669 1 ((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm3.1  704  xoranor  1309  difindiss  3236
  Copyright terms: Public domain W3C validator