Theorem pm4.24 571

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

Syntax hints:   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anidm  572  anabsan  675  nic-ax  1692  sbnf2  2388  euind  3685  reuind  3714  disjprg  5093  wesn  5732  01sqrexlem5  15264  srg1zr  20252  crngunit  20414  lmodvscl  20933  isclo2  23136  vitalilem1  25658  tgjustf  28630  ercgrg  28674  slmdvscl  33355  erler  33407  in-ax8  36545  bj-imdirco  37643  idinxpssinxp2  38784  eldmcoss2  39009  prtlem16  39454  prjsperref  43149  omabs2  43870  ifpid1g  44031  opabbrfex0d  47841  opabbrfexd  47843