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

Theorem pm2.24 621
Description: Theorem *2.24 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
Assertion
Ref Expression
pm2.24 (𝜑 → (¬ 𝜑𝜓))

Proof of Theorem pm2.24
StepHypRef Expression
1 pm2.21 617 . 2 𝜑 → (𝜑𝜓))
21com12 30 1 (𝜑 → (¬ 𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in2 615
This theorem is referenced by:  pm2.24d  622  pm2.53  722  pm2.82  812  pm4.81dc  908  dedlema  969  alexim  1645  eqneqall  2357  elnelall  2454  sotritric  4325  ltxrlt  8023  zltnle  9299  elfzonlteqm1  10210  qltnle  10246  hashfzp1  10804  dfgcd2  12015  oddprmdvds  12352  bj-fast  14496  nnnotnotr  14745
  Copyright terms: Public domain W3C validator