MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm4.24 Structured version   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  |-  ( ph  <->  (
ph  /\  ph ) )

Proof of Theorem pm4.24
StepHypRef Expression
1 id 22 . 2  |-  ( ph  ->  ph )
21pm4.71i 632 1  |-  ( ph  <->  (
ph  /\  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369
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
This theorem is referenced by:  anidm  644  anabsan  811  nic-ax  1490  sbnf2  2166  euind  3295  reuind  3312  disjprg  4449  wesn  5077  sqrlem5  13060  srg1zr  17052  crngunit  17183  lmodvscl  17400  isclo2  19457  vitalilem1  21885  ercgrg  23774  slmdvscl  27581  prtlem16  30538
  Copyright terms: Public domain W3C validator