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 565
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 561 1 (𝜑 ↔ (𝜑𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397
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 206  df-an 398
This theorem is referenced by:  anidm  566  anabsan  664  nic-ax  1676  sbnf2  2355  euind  3686  reuind  3715  disjprgw  5104  disjprg  5105  wesn  5724  01sqrexlem5  15140  srg1zr  19954  crngunit  20099  lmodvscl  20383  isclo2  22462  vitalilem1  24995  tgjustf  27464  ercgrg  27508  slmdvscl  32105  bj-imdirco  35711  idinxpssinxp2  36829  eldmcoss2  36971  prtlem16  37381  prjsperref  40991  omabs2  41714  ifpid1g  41858  opabbrfex0d  45608  opabbrfexd  45610
  Copyright terms: Public domain W3C validator