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

Step	Hyp	Ref	Expression
1		id 22	. 2
2	1	pm4.71i 632	1

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