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

Theorem pm4.24 643
Description: Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.)
Assertion
Ref Expression
pm4.24

Proof of Theorem pm4.24
StepHypRef Expression
1 id 22 . 2
21pm4.71i 632 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369
This theorem is referenced by:  anidm  644  anabsan  809  nic-ax  1481  sbnf2  2153  euind  3256  reuind  3273  disjprg  4405  wesn  5027  sqrlem5  12894  crngunit  16930  lmodvscl  17141  isclo2  19091  vitalilem1  21488  ercgrg  23372  slmdvscl  26691  prtlem16  29474
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-an 371
  Copyright terms: Public domain W3C validator