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

Theorem pm2.53 848
 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 845 . 2 ((𝜑𝜓) ↔ (¬ 𝜑𝜓))
21biimpi 219 1 ((𝜑𝜓) → (¬ 𝜑𝜓))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 844 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 210  df-or 845 This theorem is referenced by:  jaoi  854  mtord  877  orel1  886  orim12dALT  909  biorfi  936  pm2.63  938  pm2.8  970  19.30  1883  19.33b  1887  r19.30  3259  soxp  7835  xnn0nnn0pnf  12033  iccpnfcnv  23660  elpreq  30415  xlt2addrd  30619  xrge0iifcnv  31418  expdioph  40383  pm10.57  41494  vk15.4j  41653  vk15.4jVD  42039  sineq0ALT  42062  xrnmnfpnf  42138  disjinfi  42236  xrlexaddrp  42398  xrred  42411  xrnpnfmnf  42526  sumnnodd  42684  stoweidlem39  43093  dirkercncflem2  43158  fourierdlem101  43261  fourierswlem  43284  salexct  43386
 Copyright terms: Public domain W3C validator