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 852
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 849 . 2 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
21biimpi 216 1 ((𝜑𝜓) → (¬ 𝜑𝜓))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 848
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 207  df-or 849
This theorem is referenced by:  jaoi  858  mtord  880  orel1  889  orim12dALT  912  biorfriOLD  941  pm2.63  943  pm2.8  975  19.30  1881  19.33b  1885  r19.30  3120  r19.30OLD  3121  soxp  8154  xnn0nnn0pnf  12612  iccpnfcnv  24975  nnsge1  28346  elpreq  32548  xlt2addrd  32762  xrge0iifcnv  33932  expdioph  43035  pm10.57  44390  vk15.4j  44548  vk15.4jVD  44934  sineq0ALT  44957  xrnmnfpnf  45088  disjinfi  45197  xrlexaddrp  45363  xrred  45376  xrnpnfmnf  45485  sumnnodd  45645  stoweidlem39  46054  dirkercncflem2  46119  fourierdlem101  46222  fourierswlem  46245  salexct  46349
  Copyright terms: Public domain W3C validator