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  665  nic-ax  1674  sbnf2  2362  euind  3682  reuind  3711  disjprg  5094  wesn  5713  01sqrexlem5  15169  srg1zr  20150  crngunit  20314  lmodvscl  20829  isclo2  23032  vitalilem1  25565  tgjustf  28545  ercgrg  28589  slmdvscl  33296  erler  33347  in-ax8  36418  bj-imdirco  37395  idinxpssinxp2  38517  eldmcoss2  38722  prtlem16  39129  prjsperref  42849  omabs2  43574  ifpid1g  43735  opabbrfex0d  47532  opabbrfexd  47534