Theorem pm4.24 675

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

Syntax hints:   ↔ wb 196   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  anidm  676  anabsan  854  nic-ax  1598  sbnf2  2439  euind  3393  reuind  3411  disjprg  4648  wesn  5190  sqrlem5  13987  srg1zr  18529  crngunit  18662  lmodvscl  18880  isclo2  20892  vitalilem1  23376  vitalilem1OLD  23377  ercgrg  25412  slmdvscl  29767  idinxpssinxp2  34089  prtlem16  34154  ifpid1g  37839  opabbrfex0d  41305  opabbrfexd  41307