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 563 | 1 ⊢ (𝜑 ↔ (𝜑 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 |
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 210 df-an 400 |
This theorem is referenced by: anidm 568 anabsan 665 nornotOLD 1531 nic-ax 1681 sbnf2 2357 euind 3637 reuind 3666 disjprgw 5048 disjprg 5049 wesn 5637 sqrlem5 14810 srg1zr 19544 crngunit 19680 lmodvscl 19916 isclo2 21985 vitalilem1 24505 tgjustf 26564 ercgrg 26608 slmdvscl 31186 bj-imdirco 35096 idinxpssinxp2 36190 eldmcoss2 36314 prtlem16 36620 prjsperref 40153 ifpid1g 40786 opabbrfex0d 44450 opabbrfexd 44452 |
Copyright terms: Public domain | W3C validator |