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  3720  reuind  3749  disjprgw  5143  disjprg  5144  wesn  5763  01sqrexlem5  15190  srg1zr  20032  crngunit  20185  lmodvscl  20482  isclo2  22584  vitalilem1  25117  tgjustf  27714  ercgrg  27758  slmdvscl  32347  bj-imdirco  36060  idinxpssinxp2  37176  eldmcoss2  37318  prtlem16  37728  prjsperref  41345  omabs2  42068  ifpid1g  42231  opabbrfex0d  45981  opabbrfexd  45983
  Copyright terms: Public domain W3C validator