![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > 3exp2 | Structured version Unicode version |
Description: Exportation from right triple conjunction. (Contributed by NM, 26-Oct-2006.) |
Ref | Expression |
---|---|
3exp2.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3exp2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp2.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ex 434 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 3expd 1205 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
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 185 df-an 371 df-3an 967 |
This theorem is referenced by: 3anassrs 1210 pm2.61da3ne 2771 po2nr 4761 fliftfund 6114 frfi 7667 fin33i 8648 axdc3lem4 8732 iscatd 14729 isfuncd 14893 isposd 15243 pospropd 15422 imasmnd2 15576 grpinveu 15690 grpid 15691 imasgrp2 15788 dmdprdd 16602 pgpfac1lem5 16701 imasrng 16833 islmodd 17076 lmodvsghm 17128 islssd 17139 islmhm2 17241 psrbaglefi 17563 psrbaglefiOLD 17564 mulgghm2 18049 mulgghm2OLD 18052 isphld 18207 riinopn 18652 ordtbaslem 18923 subbascn 18989 haust1 19087 isnrm2 19093 isnrm3 19094 lmmo 19115 nllyidm 19224 tx1stc 19354 filin 19558 filtop 19559 isfil2 19560 infil 19567 fgfil 19579 isufil2 19612 ufileu 19623 filufint 19624 flimopn 19679 flimrest 19687 isxmetd 20032 met2ndc 20229 icccmplem2 20531 lmmbr 20900 cfil3i 20911 equivcfil 20941 bcthlem5 20970 volfiniun 21160 dvidlem 21522 ulmdvlem3 21999 ax5seg 23335 axcontlem4 23364 axcont 23373 grporcan 23859 grpoinveu 23860 grpoid 23861 grpoasscan1 23875 cvxpcon 27274 cvxscon 27275 predpo 27788 broutsideof2 28296 nn0prpwlem 28664 fgmin 28738 cntotbnd 28842 heiborlem6 28862 heiborlem10 28866 rngonegmn1l 28902 rngonegmn1r 28903 rngoneglmul 28904 rngonegrmul 28905 crngm23 28949 prnc 29014 pridlc3 29020 dmncan1 29023 lsmsat 32976 eqlkr 33067 llncmp 33489 2at0mat0 33492 llncvrlpln 33525 lplncmp 33529 lplnexllnN 33531 lplncvrlvol 33583 lvolcmp 33584 linepsubN 33719 pmapsub 33735 paddasslem16 33802 pmodlem2 33814 lhp2lt 33968 ltrneq2 34115 cdlemf2 34529 cdlemk34 34877 cdlemn11pre 35178 dihord2pre 35193 |
Copyright terms: Public domain | W3C validator |