Theorem pm4.24 568

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

Syntax hints:   ↔ wb 207   ∧ 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 208  df-an 397

This theorem is referenced by:  anidm  569  anabsan  671  nic-ax  1680  sbnf2  2366  euind  3672  reuind  3701  disjprg  5075  wesn  5714  01sqrexlem5  15206  srg1zr  20194  crngunit  20356  lmodvscl  20875  isclo2  23078  vitalilem1  25600  tgjustf  28566  ercgrg  28610  slmdvscl  33302  erler  33353  in-ax8  36459  bj-imdirco  37557  idinxpssinxp2  38698  eldmcoss2  38923  prtlem16  39368  prjsperref  43063  omabs2  43784  ifpid1g  43945  opabbrfex0d  47756  opabbrfexd  47758