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  3720  reuind  3749  disjprgw  5143  disjprg  5144  wesn  5763  01sqrexlem5  15190  srg1zr  20032  crngunit  20185  lmodvscl  20482  isclo2  22584  vitalilem1  25117  tgjustf  27714  ercgrg  27758  slmdvscl  32347  bj-imdirco  36060  idinxpssinxp2  37176  eldmcoss2  37318  prtlem16  37728  prjsperref  41345  omabs2  42068  ifpid1g  42231  opabbrfex0d  45981  opabbrfexd  45983