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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2	1	pm4.71i 559	1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑))

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  666  nic-ax  1675  sbnf2  2363  euind  3684  reuind  3713  disjprg  5096  wesn  5721  01sqrexlem5  15181  srg1zr  20162  crngunit  20326  lmodvscl  20841  isclo2  23044  vitalilem1  25577  tgjustf  28557  ercgrg  28601  slmdvscl  33307  erler  33358  in-ax8  36437  bj-imdirco  37442  idinxpssinxp2  38572  eldmcoss2  38797  prtlem16  39242  prjsperref  42961  omabs2  43686  ifpid1g  43847  opabbrfex0d  47643  opabbrfexd  47645