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  664  nic-ax  1671  sbnf2  2364  euind  3746  reuind  3775  disjprg  5162  wesn  5788  01sqrexlem5  15295  srg1zr  20242  crngunit  20404  lmodvscl  20898  isclo2  23117  vitalilem1  25662  tgjustf  28499  ercgrg  28543  slmdvscl  33193  erler  33237  in-ax8  36190  bj-imdirco  37156  idinxpssinxp2  38274  eldmcoss2  38415  prtlem16  38825  prjsperref  42561  omabs2  43294  ifpid1g  43456  opabbrfex0d  47201  opabbrfexd  47203