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  15197  srg1zr  20109  crngunit  20269  lmodvscl  20632  isclo2  22812  vitalilem1  25349  tgjustf  27979  ercgrg  28023  slmdvscl  32617  bj-imdirco  36374  idinxpssinxp2  37490  eldmcoss2  37632  prtlem16  38042  prjsperref  41650  omabs2  42384  ifpid1g  42547  opabbrfex0d  46293  opabbrfexd  46295