![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > jctild | Structured version Visualization version Unicode version |
Description: Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.) |
Ref | Expression |
---|---|
jctild.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
jctild.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
jctild |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jctild.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1d 26 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | jctild.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | jcad 540 |
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 190 df-an 377 |
This theorem is referenced by: syl6an 552 anc2li 564 ordunidif 5489 isofrlem 6255 dfwe2 6634 orduniorsuc 6683 poxp 6934 fnse 6939 ssenen 7771 dffi3 7970 fpwwe2lem13 9092 zmulcl 11013 rpneg 11360 rexuz3 13459 cau3lem 13465 climrlim2 13659 o1rlimmul 13730 iseralt 13799 gcdeq 14568 isprm3 14681 vdwnnlem2 14994 ablfaclem3 17768 epttop 20072 lmcnp 20368 dfcon2 20482 txcnp 20683 cmphaushmeo 20863 isfild 20921 cnpflf2 21063 flimfnfcls 21091 alexsubALT 21114 fgcfil 22289 bcthlem5 22344 ivthlem2 22451 ivthlem3 22452 dvfsumrlim 23031 plypf1 23214 axeuclidlem 25040 wwlknredwwlkn0 25503 wwlkextwrd 25504 wwlkextproplem1 25517 clwlkisclwwlklem2a1 25555 rusgranumwlklem1 25725 numclwwlkovf2ex 25862 extwwlkfab 25866 lnon0 26487 hstles 27932 mdsl1i 28022 atcveq0 28049 atcvat4i 28098 cdjreui 28133 issgon 28993 conpcon 30006 tfisg 30505 frmin 30528 outsideofrflx 30942 isbasisrelowllem1 31802 isbasisrelowllem2 31803 poimirlem3 31987 poimirlem29 32013 poimir 32017 heicant 32019 equivtotbnd 32154 ismtybndlem 32182 cvrat4 33052 linepsubN 33361 pmapsub 33377 osumcllem4N 33568 pexmidlem1N 33579 dochexmidlem1 35072 clcnvlem 36274 2reu1 38644 iccpartimp 38768 gcdzeq 38830 bgoldbwt 38915 bgoldbst 38916 usgr2wlkneq 39787 |
Copyright terms: Public domain | W3C validator |