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  1670  sbnf2  2359  euind  3733  reuind  3762  disjprg  5144  wesn  5777  01sqrexlem5  15282  srg1zr  20233  crngunit  20395  lmodvscl  20893  isclo2  23112  vitalilem1  25657  tgjustf  28496  ercgrg  28540  slmdvscl  33203  erler  33252  in-ax8  36207  bj-imdirco  37173  idinxpssinxp2  38300  eldmcoss2  38441  prtlem16  38851  prjsperref  42593  omabs2  43322  ifpid1g  43484  opabbrfex0d  47236  opabbrfexd  47238