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 674
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 663 1 (𝜑 ↔ (𝜑𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384
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 386
This theorem is referenced by:  anidm  675  anabsan  853  nic-ax  1595  sbnf2  2438  euind  3379  reuind  3397  disjprg  4613  wesn  5156  sqrlem5  13929  srg1zr  18461  crngunit  18594  lmodvscl  18812  isclo2  20815  vitalilem1  23299  vitalilem1OLD  23300  ercgrg  25329  slmdvscl  29576  prtlem16  33669  ifpid1g  37355  opabbrfex0d  40628  opabbrfexd  40630
  Copyright terms: Public domain W3C validator