Theorem pm4.24 563

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anidm  564  anabsan  665  nic-ax  1674  sbnf2  2358  euind  3683  reuind  3712  disjprg  5087  wesn  5705  01sqrexlem5  15153  srg1zr  20134  crngunit  20297  lmodvscl  20812  isclo2  23004  vitalilem1  25537  tgjustf  28452  ercgrg  28496  slmdvscl  33181  erler  33230  in-ax8  36264  bj-imdirco  37230  idinxpssinxp2  38358  eldmcoss2  38502  prtlem16  38914  prjsperref  42645  omabs2  43371  ifpid1g  43533  opabbrfex0d  47323  opabbrfexd  47325