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 563
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 559 1 (𝜑 ↔ (𝜑𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395
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 207  df-an 396
This theorem is referenced by:  anidm  564  anabsan  665  nic-ax  1672  sbnf2  2360  euind  3729  reuind  3758  disjprg  5138  wesn  5773  01sqrexlem5  15286  srg1zr  20213  crngunit  20379  lmodvscl  20877  isclo2  23097  vitalilem1  25644  tgjustf  28482  ercgrg  28526  slmdvscl  33221  erler  33270  in-ax8  36226  bj-imdirco  37192  idinxpssinxp2  38320  eldmcoss2  38461  prtlem16  38871  prjsperref  42621  omabs2  43350  ifpid1g  43512  opabbrfex0d  47303  opabbrfexd  47305
  Copyright terms: Public domain W3C validator