Theorem pm4.24 563

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anidm  564  anabsan  665  nic-ax  1673  sbnf2  2361  euind  3712  reuind  3741  disjprg  5120  wesn  5748  01sqrexlem5  15270  srg1zr  20180  crngunit  20343  lmodvscl  20840  isclo2  23031  vitalilem1  25566  tgjustf  28457  ercgrg  28501  slmdvscl  33216  erler  33265  in-ax8  36247  bj-imdirco  37213  idinxpssinxp2  38341  eldmcoss2  38482  prtlem16  38892  prjsperref  42596  omabs2  43323  ifpid1g  43485  opabbrfex0d  47282  opabbrfexd  47284