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 387
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 384 . 2 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
21biimpi 206 1 ((𝜑𝜓) → (¬ 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 382
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 197  df-or 384
This theorem is referenced by:  jaoi  393  orel1  396  pm2.63  846  pm2.8  913  19.30  1849  19.33b  1853  soxp  7335  xnn0nnn0pnf  11414  iccpnfcnv  22790  elpreq  29486  xlt2addrd  29651  xrge0iifcnv  30107  expdioph  37907  pm10.57  38887  vk15.4j  39051  vk15.4jVD  39464  sineq0ALT  39487  xrnmnfpnf  39570  disjinfi  39694  xrlexaddrp  39881  xrred  39894  xrnpnfmnf  40018  sumnnodd  40180  stoweidlem39  40574  dirkercncflem2  40639  fourierdlem101  40742  fourierswlem  40765  salexct  40870
  Copyright terms: Public domain W3C validator