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  665  nic-ax  1673  sbnf2  2356  euind  3695  reuind  3724  disjprg  5103  wesn  5727  01sqrexlem5  15212  srg1zr  20124  crngunit  20287  lmodvscl  20784  isclo2  22975  vitalilem1  25509  tgjustf  28400  ercgrg  28444  slmdvscl  33167  erler  33216  in-ax8  36212  bj-imdirco  37178  idinxpssinxp2  38306  eldmcoss2  38450  prtlem16  38862  prjsperref  42594  omabs2  43321  ifpid1g  43483  opabbrfex0d  47284  opabbrfexd  47286