Theorem pm4.24 573

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  anidm  574  anabsan  677  nic-ax  1703  sbnf2  2390  euind  3688  reuind  3717  disjprg  5106  wesn  5752  01sqrexlem5  15299  rng1zrlem  20260  crngunit  20461  lmodvscl  20980  isclo2  23226  vitalilem1  25748  tgjustf  28723  ercgrg  28767  slmdvscl  33515  erler  33566  in-ax8  36717  bj-imdirco  37815  idinxpssinxp2  38954  eldmcoss2  39179  prtlem16  39624  prjsperref  43321  omabs2  44042  ifpid1g  44203  opabbrfex0d  48006  opabbrfexd  48008  2alsraln0id  50579