Theorem pm4.24 573

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 23	. 2 ⊢ (𝜑 → 𝜑)
2	1	pm4.71i 568	1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑))

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anidm  574  anabsan  677  nic-ax  1700  sbnf2  2396  euind  3696  reuind  3725  disjprg  5106  wesn  5748  01sqrexlem5  15293  rng1zrlem  20255  crngunit  20456  lmodvscl  20973  isclo2  23210  vitalilem1  25732  tgjustf  28704  ercgrg  28748  slmdvscl  33471  erler  33522  in-ax8  36621  bj-imdirco  37717  idinxpssinxp2  38858  eldmcoss2  39083  prtlem16  39528  prjsperref  43223  omabs2  43944  ifpid1g  44105  opabbrfex0d  47905  opabbrfexd  47907