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 205   ∧ 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 206  df-an 396

This theorem is referenced by:  anidm  564  anabsan  661  nornotOLD  1527  nic-ax  1677  sbnf2  2356  euind  3654  reuind  3683  disjprgw  5065  disjprg  5066  wesn  5666  sqrlem5  14886  srg1zr  19680  crngunit  19819  lmodvscl  20055  isclo2  22147  vitalilem1  24677  tgjustf  26738  ercgrg  26782  slmdvscl  31369  bj-imdirco  35288  idinxpssinxp2  36380  eldmcoss2  36504  prtlem16  36810  prjsperref  40366  ifpid1g  40999  opabbrfex0d  44665  opabbrfexd  44667