Theorem pm4.24 574

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 23	. 2 ⊢ (𝜑 → 𝜑)
2	1	pm4.71i 569	1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anidm  575  anabsan  678  nic-ax  1706  sbnf2  2387  euind  3682  reuind  3711  disjprg  5099  wesn  5744  01sqrexlem5  15333  rng1zrlem  20316  crngunit  20519  lmodvscl  21062  isclo2  23313  vitalilem1  25836  tgjustf  28814  ercgrg  28859  slmdvscl  33654  erler  33705  in-ax8  36844  bj-imdirco  37942  idinxpssinxp2  39072  eldmcoss2  39297  prtlem16  39742  prjsperref  43452  omabs2  44173  ifpid1g  44334  opabbrfex0d  48174  opabbrfexd  48176  2alsraln0id  50747