|   | 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 559 | 1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑)) | 
| Colors of variables: wff setvar class | 
| 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 1672 sbnf2 2360 euind 3729 reuind 3758 disjprg 5138 wesn 5773 01sqrexlem5 15286 srg1zr 20213 crngunit 20379 lmodvscl 20877 isclo2 23097 vitalilem1 25644 tgjustf 28482 ercgrg 28526 slmdvscl 33221 erler 33270 in-ax8 36226 bj-imdirco 37192 idinxpssinxp2 38320 eldmcoss2 38461 prtlem16 38871 prjsperref 42621 omabs2 43350 ifpid1g 43512 opabbrfex0d 47303 opabbrfexd 47305 | 
| Copyright terms: Public domain | W3C validator |