Theorem pm4.24 673

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

Syntax hints:   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  anidm  674  anabsan  850  nic-ax  1589  sbnf2  2427  euind  3360  reuind  3378  disjprg  4578  wesn  5113  sqrlem5  13835  srg1zr  18352  crngunit  18485  lmodvscl  18703  isclo2  20702  vitalilem1  23182  vitalilem1OLD  23183  ercgrg  25212  slmdvscl  29098  prtlem16  33172  ifpid1g  36858  opabbrfex0d  40331  opabbrfexd  40333