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  1672  sbnf2  2360  euind  3729  reuind  3758  disjprg  5138  wesn  5773  01sqrexlem5  15286  srg1zr  20213  crngunit  20379  lmodvscl  20877  isclo2  23097  vitalilem1  25644  tgjustf  28482  ercgrg  28526  slmdvscl  33221  erler  33270  in-ax8  36226  bj-imdirco  37192  idinxpssinxp2  38320  eldmcoss2  38461  prtlem16  38871  prjsperref  42621  omabs2  43350  ifpid1g  43512  opabbrfex0d  47303  opabbrfexd  47305