Theorem pm4.24 567

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

Syntax hints:   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anidm  568  anabsan  665  nornotOLD  1531  nic-ax  1681  sbnf2  2357  euind  3637  reuind  3666  disjprgw  5048  disjprg  5049  wesn  5637  sqrlem5  14810  srg1zr  19544  crngunit  19680  lmodvscl  19916  isclo2  21985  vitalilem1  24505  tgjustf  26564  ercgrg  26608  slmdvscl  31186  bj-imdirco  35096  idinxpssinxp2  36190  eldmcoss2  36314  prtlem16  36620  prjsperref  40153  ifpid1g  40786  opabbrfex0d  44450  opabbrfexd  44452