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  1706  sbnf2  2388  euind  3682  reuind  3711  disjprg  5099  wesn  5740  01sqrexlem5  15406  rng1zrlem  20396  crngunit  20601  lmodvscl  21146  isclo2  23399  vitalilem1  25922  tgjustf  28928  ercgrg  28973  slmdvscl  33768  erler  33819  in-ax8  36993  bj-imdirco  38091  idinxpssinxp2  39236  eldmcoss2  39461  prtlem16  39906  prjsperref  43614  omabs2  44318  ifpid1g  44479  opabbrfex0d  48325  opabbrfexd  48327  2alsraln0id  50883