Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > jctild | Structured version Visualization version GIF 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 25 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
3 | jctild.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
4 | 2, 3 | jcad 513 | 1 ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: anc2li 556 equvini 2472 2reu1 3880 ordunidif 6233 isofrlem 7082 dfwe2 7484 orduniorsuc 7533 poxp 7813 fnse 7818 ssenen 8680 dffi3 8884 fpwwe2lem13 10053 zmulcl 12020 rpneg 12411 rexuz3 14698 cau3lem 14704 climrlim2 14894 o1rlimmul 14965 iseralt 15031 gcdzeq 15892 isprm3 16017 vdwnnlem2 16322 ablfaclem3 19140 epttop 21547 lmcnp 21842 dfconn2 21957 txcnp 22158 cmphaushmeo 22338 isfild 22396 cnpflf2 22538 flimfnfcls 22566 alexsubALT 22589 fgcfil 23803 bcthlem5 23860 ivthlem2 23982 ivthlem3 23983 dvfsumrlim 24557 plypf1 24731 axeuclidlem 26676 usgr2wlkneq 27465 wwlksnredwwlkn0 27602 wwlksnextwrd 27603 clwlkclwwlklem2a1 27698 lnon0 28503 hstles 29936 mdsl1i 30026 atcveq0 30053 atcvat4i 30102 cdjreui 30137 issgon 31282 connpconn 32380 tfisg 32953 frpoinsg 32979 frmin 32982 outsideofrflx 33486 isbasisrelowllem1 34519 isbasisrelowllem2 34520 poimirlem3 34777 poimirlem29 34803 poimir 34807 heicant 34809 equivtotbnd 34939 ismtybndlem 34967 cvrat4 36461 linepsubN 36770 pmapsub 36786 osumcllem4N 36977 pexmidlem1N 36988 dochexmidlem1 38478 harval3 39784 clcnvlem 39863 iccpartimp 43424 sbgoldbwt 43789 sbgoldbst 43790 elsetrecslem 44699 |
Copyright terms: Public domain | W3C validator |