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  2360  euind  3679  reuind  3708  disjprg  5091  wesn  5710  01sqrexlem5  15157  srg1zr  20137  crngunit  20300  lmodvscl  20815  isclo2  23006  vitalilem1  25539  tgjustf  28454  ercgrg  28498  slmdvscl  33192  erler  33241  in-ax8  36291  bj-imdirco  37257  idinxpssinxp2  38379  eldmcoss2  38584  prtlem16  38991  prjsperref  42727  omabs2  43452  ifpid1g  43614  opabbrfex0d  47413  opabbrfexd  47415