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  2362  euind  3670  reuind  3699  disjprg  5081  wesn  5720  01sqrexlem5  15208  srg1zr  20196  crngunit  20358  lmodvscl  20873  isclo2  23053  vitalilem1  25575  tgjustf  28541  ercgrg  28585  slmdvscl  33275  erler  33326  in-ax8  36406  bj-imdirco  37504  idinxpssinxp2  38645  eldmcoss2  38870  prtlem16  39315  prjsperref  43039  omabs2  43760  ifpid1g  43921  opabbrfex0d  47734  opabbrfexd  47736