Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > pm3.22 | Structured version Visualization version Unicode version |
Description: Theorem *3.22 of [WhiteheadRussell] p. 111. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Nov-2012.) |
Ref | Expression |
---|---|
pm3.22 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.21 464 | . 2 | |
2 | 1 | imp 445 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 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: ancom 466 ancom2s 844 ancom1s 847 fi1uzind 13279 fi1uzindOLD 13285 cshwlen 13545 prmgapprmolem 15765 setsstructOLD 15899 mat1dimcrng 20283 dmatcrng 20308 cramerlem1 20493 cramer 20497 pmatcollpwscmatlem2 20595 uhgr3cyclex 27042 3cyclfrgrrn 27150 frgrreggt1 27251 grpoidinvlem3 27360 atomli 29241 arg-ax 32415 cnambfre 33458 prter1 34164 eliuniincex 39292 eliincex 39293 dvdsn1add 40154 fourierdlem42 40366 fourierdlem80 40403 etransclem38 40489 gbegt5 41649 c0snmhm 41915 pgrpgt2nabl 42147 |
Copyright terms: Public domain | W3C validator |