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 553
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 549 1 (𝜑 ↔ (𝜑𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382
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 383
This theorem is referenced by:  anidm  554  anabsan  644  nic-ax  1746  sbnf2  2589  euind  3545  reuind  3563  disjprg  4783  wesn  5329  sqrlem5  14194  srg1zr  18736  crngunit  18869  lmodvscl  19089  isclo2  21112  vitalilem1  23595  ercgrg  25632  slmdvscl  30106  idinxpssinxp2  34431  eldmcoss2  34550  prtlem16  34676  ifpid1g  38365  opabbrfex0d  41825  opabbrfexd  41827
  Copyright terms: Public domain W3C validator