![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm4.24 | Structured version Visualization version GIF version |
Description: Theorem *4.24 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.) |
Ref | Expression |
---|---|
pm4.24 | ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝜑 → 𝜑) | |
2 | 1 | pm4.71i 561 | 1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 |
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 206 df-an 398 |
This theorem is referenced by: anidm 566 anabsan 664 nic-ax 1676 sbnf2 2355 euind 3720 reuind 3749 disjprgw 5143 disjprg 5144 wesn 5763 01sqrexlem5 15190 srg1zr 20032 crngunit 20185 lmodvscl 20482 isclo2 22584 vitalilem1 25117 tgjustf 27714 ercgrg 27758 slmdvscl 32347 bj-imdirco 36060 idinxpssinxp2 37176 eldmcoss2 37318 prtlem16 37728 prjsperref 41345 omabs2 42068 ifpid1g 42231 opabbrfex0d 45981 opabbrfexd 45983 |
Copyright terms: Public domain | W3C validator |