Theorem pm4.24 564

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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  anidm  565  anabsan  662  nic-ax  1676  sbnf2  2356  euind  3659  reuind  3688  disjprgw  5069  disjprg  5070  wesn  5675  sqrlem5  14958  srg1zr  19765  crngunit  19904  lmodvscl  20140  isclo2  22239  vitalilem1  24772  tgjustf  26834  ercgrg  26878  slmdvscl  31467  bj-imdirco  35361  idinxpssinxp2  36453  eldmcoss2  36577  prtlem16  36883  prjsperref  40445  ifpid1g  41101  opabbrfex0d  44778  opabbrfexd  44780