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  2392  euind  3689  reuind  3718  disjprg  5107  wesn  5752  01sqrexlem5  15316  rng1zrlem  20282  crngunit  20485  lmodvscl  21028  isclo2  23274  vitalilem1  25796  tgjustf  28771  ercgrg  28815  slmdvscl  33557  erler  33608  in-ax8  36769  bj-imdirco  37867  idinxpssinxp2  39006  eldmcoss2  39231  prtlem16  39676  prjsperref  43371  omabs2  44092  ifpid1g  44253  opabbrfex0d  48056  opabbrfexd  48058  2alsraln0id  50629