Theorem pm4.24 566

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

Syntax hints:   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anidm  567  anabsan  663  nornotOLD  1525  nic-ax  1674  sbnf2  2377  euind  3717  reuind  3746  disjprgw  5063  disjprg  5064  wesn  5642  sqrlem5  14608  srg1zr  19281  crngunit  19414  lmodvscl  19653  isclo2  21698  vitalilem1  24211  tgjustf  26261  ercgrg  26305  slmdvscl  30844  idinxpssinxp2  35577  eldmcoss2  35701  prtlem16  36007  prjsperref  39263  ifpid1g  39867  opabbrfex0d  43492  opabbrfexd  43494