Theorem pm4.24 564

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

Syntax hints:   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  anidm  565  anabsan  661  nornot  1516  nic-ax  1655  sbnf2  2334  euind  3649  reuind  3678  disjprg  4958  wesn  5526  sqrlem5  14440  srg1zr  18969  crngunit  19102  lmodvscl  19341  isclo2  21380  vitalilem1  23892  tgjustf  25941  ercgrg  25985  slmdvscl  30480  idinxpssinxp2  35107  eldmcoss2  35230  prtlem16  35536  prjsperref  38753  ifpid1g  39345  opabbrfex0d  43001  opabbrfexd  43003