Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3imp1 | Structured version Visualization version Unicode version |
Description: Importation to left triple conjunction. (Contributed by NM, 24-Feb-2005.) |
Ref | Expression |
---|---|
3imp1.1 |
Ref | Expression |
---|---|
3imp1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3imp1.1 | . . 3 | |
2 | 1 | 3imp 1256 | . 2 |
3 | 2 | imp 445 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 w3a 1037 |
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 df-3an 1039 |
This theorem is referenced by: reupick2 3913 indcardi 8864 ledivge1le 11901 expcan 12913 ltexp2 12914 leexp1a 12919 expnbnd 12993 cshf1 13556 rtrclreclem4 13801 relexpindlem 13803 ncoprmlnprm 15436 xrsdsreclblem 19792 matecl 20231 scmateALT 20318 riinopn 20713 neindisj2 20927 filufint 21724 tsmsxp 21958 ewlkle 26501 uspgr2wlkeq 26542 spthonepeq 26648 wwlksm1edg 26767 clwwlkinwwlk 26905 clwwisshclwws 26928 3vfriswmgr 27142 clwwlksnwwlksn 27209 homco1 28660 homulass 28661 hoadddir 28663 mblfinlem3 33448 zerdivemp1x 33746 athgt 34742 psubspi 35033 paddasslem14 35119 eluzge0nn0 41322 iccpartigtl 41359 lighneal 41528 |
Copyright terms: Public domain | W3C validator |