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

Theorem pm2.53 373
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 370 . 2
21biimpi 194 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  \/wo 368
This theorem is referenced by:  jaoi  379  orel1  382  pm2.63  788  pm2.8  850  19.30  1692  19.33b  1696  soxp  6913  iccpnfcnv  21444  elpreq  27417  xlt2addrd  27578  xrge0iifcnv  27915  expdioph  30965  pm10.57  31276  sumnnodd  31636  stoweidlem39  31821  dirkercncflem2  31886  fourierdlem101  31990  fourierswlem  32013  vk15.4j  33298  vk15.4jVD  33714  sineq0ALT  33737
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 185  df-or 370
  Copyright terms: Public domain W3C validator