Theorem pm4.24 564

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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  anidm  565  anabsan  663  nic-ax  1675  sbnf2  2354  euind  3720  reuind  3749  disjprgw  5143  disjprg  5144  wesn  5764  01sqrexlem5  15192  srg1zr  20037  crngunit  20191  lmodvscl  20488  isclo2  22591  vitalilem1  25124  tgjustf  27721  ercgrg  27765  slmdvscl  32354  bj-imdirco  36066  idinxpssinxp2  37182  eldmcoss2  37324  prtlem16  37734  prjsperref  41349  omabs2  42072  ifpid1g  42235  opabbrfex0d  45984  opabbrfexd  45986