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

Theorem pm4.24 647
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 636 1  |-  ( ph  <->  (
ph  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  anidm  648  anabsan  820  nic-ax  1550  sbnf2  2238  euind  3257  reuind  3275  disjprg  4419  wesn  4925  sqrlem5  13310  srg1zr  17761  crngunit  17889  lmodvscl  18107  isclo2  20102  vitalilem1  22564  ercgrg  24560  slmdvscl  28537  prtlem16  32409  ifpid1g  36108
  Copyright terms: Public domain W3C validator