Theorem pm4.24 574

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 569	1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anidm  575  anabsan  678  nic-ax  1705  sbnf2  2387  euind  3681  reuind  3710  disjprg  5098  wesn  5739  01sqrexlem5  15419  rng1zrlem  20409  crngunit  20614  lmodvscl  21159  isclo2  23412  vitalilem1  25935  tgjustf  28941  ercgrg  28986  slmdvscl  33822  erler  33873  in-ax8  37106  bj-imdirco  38205  idinxpssinxp2  39350  eldmcoss2  39575  prtlem16  40020  prjsperref  43728  omabs2  44428  ifpid1g  44589  opabbrfex0d  48450  opabbrfexd  48452  2alsraln0id  51083