MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.53 Structured version   Visualization version   GIF version

Theorem pm2.53 847
Description: Theorem *2.53 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
Assertion
Ref Expression
pm2.53 ((𝜑𝜓) → (¬ 𝜑𝜓))

Proof of Theorem pm2.53
StepHypRef Expression
1 df-or 844 . 2 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
21biimpi 217 1 ((𝜑𝜓) → (¬ 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 843
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 208  df-or 844
This theorem is referenced by:  jaoi  853  mtord  875  orel1  884  orim12dALT  907  biorfi  934  pm2.63  936  pm2.8  968  19.30  1875  19.33b  1879  r19.30  3342  soxp  7817  xnn0nnn0pnf  11972  iccpnfcnv  23465  elpreq  30206  xlt2addrd  30397  xrge0iifcnv  31064  expdioph  39487  pm10.57  40570  vk15.4j  40729  vk15.4jVD  41115  sineq0ALT  41138  xrnmnfpnf  41214  disjinfi  41321  xrlexaddrp  41487  xrred  41500  xrnpnfmnf  41618  sumnnodd  41778  stoweidlem39  42192  dirkercncflem2  42257  fourierdlem101  42360  fourierswlem  42383  salexct  42485
  Copyright terms: Public domain W3C validator