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  2388  euind  3682  reuind  3711  disjprg  5099  wesn  5740  01sqrexlem5  15413  rng1zrlem  20403  crngunit  20608  lmodvscl  21153  isclo2  23406  vitalilem1  25929  tgjustf  28935  ercgrg  28980  slmdvscl  33775  erler  33826  in-ax8  37013  bj-imdirco  38111  idinxpssinxp2  39256  eldmcoss2  39481  prtlem16  39926  prjsperref  43634  omabs2  44333  ifpid1g  44494  opabbrfex0d  48355  opabbrfexd  48357  2alsraln0id  50913