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  2390  euind  3685  reuind  3714  disjprg  5104  wesn  5748  01sqrexlem5  15456  rng1zrlem  20454  crngunit  20659  lmodvscl  21204  isclo2  23461  vitalilem1  25984  tgjustf  28992  ercgrg  29037  slmdvscl  33874  erler  33925  in-ax8  37228  bj-imdirco  38379  idinxpssinxp2  39522  eldmcoss2  39747  prtlem16  40192  prjsperref  43900  omabs2  44595  ifpid1g  44756  opabbrfex0d  48629  opabbrfexd  48631  2alsraln0id  51342