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

Theorem pm4.24 641
Description: Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.)
Assertion
Ref Expression
pm4.24  |-  ( ph  <->  (
ph  /\  ph ) )

Proof of Theorem pm4.24
StepHypRef Expression
1 id 22 . 2  |-  ( ph  ->  ph )
21pm4.71i 630 1  |-  ( ph  <->  (
ph  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367
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 369
This theorem is referenced by:  anidm  642  anabsan  811  nic-ax  1513  sbnf2  2187  euind  3211  reuind  3228  disjprg  4363  wesn  4985  sqrlem5  13082  srg1zr  17293  crngunit  17424  lmodvscl  17642  isclo2  19675  vitalilem1  22102  ercgrg  24028  slmdvscl  27910  prtlem16  30776  ifpid1g  38122
  Copyright terms: Public domain W3C validator