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

Theorem pm4.24 676
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 665 1 (𝜑 ↔ (𝜑𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383
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 197  df-an 385
This theorem is referenced by:  anidm  677  anabsan  871  nic-ax  1638  sbnf2  2467  euind  3426  reuind  3444  disjprg  4680  wesn  5224  sqrlem5  14031  srg1zr  18575  crngunit  18708  lmodvscl  18928  isclo2  20940  vitalilem1  23422  ercgrg  25457  slmdvscl  29895  idinxpssinxp2  34230  eldmcoss2  34349  prtlem16  34473  ifpid1g  38156  opabbrfex0d  41628  opabbrfexd  41630
  Copyright terms: Public domain W3C validator