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 849
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 846 . 2 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
21biimpi 215 1 ((𝜑𝜓) → (¬ 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 845
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 206  df-or 846
This theorem is referenced by:  jaoi  855  mtord  878  orel1  887  orim12dALT  910  biorfi  937  pm2.63  939  pm2.8  971  19.30  1884  19.33b  1888  r19.30  3121  r19.30OLD  3122  soxp  8057  xnn0nnn0pnf  12494  iccpnfcnv  24291  elpreq  31343  xlt2addrd  31546  xrge0iifcnv  32383  expdioph  41285  pm10.57  42593  vk15.4j  42752  vk15.4jVD  43138  sineq0ALT  43161  xrnmnfpnf  43235  disjinfi  43348  xrlexaddrp  43522  xrred  43535  xrnpnfmnf  43646  sumnnodd  43803  stoweidlem39  44212  dirkercncflem2  44277  fourierdlem101  44380  fourierswlem  44403  salexct  44507
  Copyright terms: Public domain W3C validator