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  3671  reuind  3700  disjprg  5082  wesn  5713  01sqrexlem5  15199  srg1zr  20187  crngunit  20349  lmodvscl  20864  isclo2  23063  vitalilem1  25585  tgjustf  28555  ercgrg  28599  slmdvscl  33290  erler  33341  in-ax8  36422  bj-imdirco  37520  idinxpssinxp2  38659  eldmcoss2  38884  prtlem16  39329  prjsperref  43053  omabs2  43778  ifpid1g  43939  opabbrfex0d  47746  opabbrfexd  47748