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

Theorem pm3.14 669
 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 798. The converse holds for decidable propositions, as seen at pm3.13dc 865. (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 102 . . 3 ((φ ψ) → φ)
21con3i 561 . 2 φ → ¬ (φ ψ))
3 simpr 103 . . 3 ((φ ψ) → ψ)
43con3i 561 . 2 ψ → ¬ (φ ψ))
52, 4jaoi 635 1 ((¬ φ ¬ ψ) → ¬ (φ ψ))
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ∨ wo 628 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  pm3.1  670  xoranor  1267  difindiss  3185
 Copyright terms: Public domain W3C validator