Theorem pm4.24 563

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anidm  564  anabsan  666  nic-ax  1675  sbnf2  2363  euind  3684  reuind  3713  disjprg  5096  wesn  5723  01sqrexlem5  15183  srg1zr  20167  crngunit  20331  lmodvscl  20846  isclo2  23049  vitalilem1  25582  tgjustf  28563  ercgrg  28607  slmdvscl  33314  erler  33365  in-ax8  36446  bj-imdirco  37472  idinxpssinxp2  38604  eldmcoss2  38829  prtlem16  39274  prjsperref  42993  omabs2  43718  ifpid1g  43879  opabbrfex0d  47675  opabbrfexd  47677