Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm4.24 | Structured version Visualization version Unicode 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 664 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wa 384 |
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 197 df-an 386 |
This theorem is referenced by: anidm 676 anabsan 854 nic-ax 1598 sbnf2 2439 euind 3393 reuind 3411 disjprg 4648 wesn 5190 sqrlem5 13987 srg1zr 18529 crngunit 18662 lmodvscl 18880 isclo2 20892 vitalilem1 23376 vitalilem1OLD 23377 ercgrg 25412 slmdvscl 29767 idinxpssinxp2 34089 prtlem16 34154 ifpid1g 37839 opabbrfex0d 41305 opabbrfexd 41307 |
Copyright terms: Public domain | W3C validator |