Theorem pm4.24 565

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

Syntax hints:   ↔ wb 205   ∧ wa 397

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 398

This theorem is referenced by:  anidm  566  anabsan  664  nic-ax  1676  sbnf2  2355  euind  3721  reuind  3750  disjprgw  5144  disjprg  5145  wesn  5765  01sqrexlem5  15193  srg1zr  20038  crngunit  20192  lmodvscl  20489  isclo2  22592  vitalilem1  25125  tgjustf  27724  ercgrg  27768  slmdvscl  32359  bj-imdirco  36071  idinxpssinxp2  37187  eldmcoss2  37329  prtlem16  37739  prjsperref  41348  omabs2  42082  ifpid1g  42245  opabbrfex0d  45994  opabbrfexd  45996