Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3imp2 | Structured version Visualization version Unicode version |
Description: Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006.) |
Ref | Expression |
---|---|
3imp1.1 |
Ref | Expression |
---|---|
3imp2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3imp1.1 | . . 3 | |
2 | 1 | 3impd 1281 | . 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: wereu 5110 ovg 6799 fisup2g 8374 fiinf2g 8406 cfcoflem 9094 ttukeylem5 9335 dedekindle 10201 grplcan 17477 mulgnnass 17576 mulgnnassOLD 17577 dmdprdsplit2 18445 mulgass2 18601 lmodvsdi 18886 lmodvsdir 18887 lmodvsass 18888 lss1d 18963 islmhm2 19038 lspsolvlem 19142 lbsextlem2 19159 cygznlem2a 19916 isphld 19999 t0dist 21129 hausnei 21132 nrmsep3 21159 fclsopni 21819 fcfneii 21841 ax5seglem5 25813 axcont 25856 grporcan 27372 grpolcan 27384 slmdvsdi 29768 slmdvsdir 29769 slmdvsass 29770 mclsppslem 31480 broutsideof2 32229 poimirlem31 33440 broucube 33443 frinfm 33530 crngm23 33801 pridl 33836 pridlc 33870 dmnnzd 33874 dmncan1 33875 paddasslem5 35110 sfprmdvdsmersenne 41520 |
Copyright terms: Public domain | W3C validator |