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

Theorem pm4.56 495
Description: Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
Assertion
Ref Expression
pm4.56

Proof of Theorem pm4.56
StepHypRef Expression
1 ioran 490 . 2
21bicomi 202 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184  \/wo 368  /\wa 369
This theorem is referenced by:  oran  496  neanior  2782  prneimg  4211  ordtri3  4919  ssxr  9675  isirred2  17350  aaliou3lem9  22746  coltr2  24028  mideulem2  24108  opphllem  24109  jm2.26lem3  30943  wopprc  30972  icccncfext  31690  cncfiooicc  31697  fourierdlem25  31914  fourierdlem35  31924  fourierswlem  32013  fouriersw  32014  etransclem44  32061  islininds2  33085  iunconlem2  33735  bj-dfbi4  34154  dalawlem13  35607  cdleme22b  36067
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  df-an 371
  Copyright terms: Public domain W3C validator