![]() |
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 512 | 1 ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 |
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 206 df-an 396 |
This theorem is referenced by: anc2li 555 equvini 2446 2reu1 3883 frpoinsg 6334 ordunidif 6403 isofrlem 7329 dfwe2 7754 orduniorsuc 7811 tfisg 7836 poxp 8108 fnse 8113 ssenen 9147 dffi3 9422 fpwwe2lem12 10633 zmulcl 12608 rpneg 13003 rexuz3 15292 cau3lem 15298 climrlim2 15488 o1rlimmul 15560 iseralt 15628 gcdzeq 16491 isprm3 16617 vdwnnlem2 16928 ablfaclem3 19999 epttop 22834 lmcnp 23130 dfconn2 23245 txcnp 23446 cmphaushmeo 23626 isfild 23684 cnpflf2 23826 flimfnfcls 23854 alexsubALT 23877 fgcfil 25121 bcthlem5 25178 ivthlem2 25303 ivthlem3 25304 dvfsumrlim 25888 plypf1 26066 noetalem1 27590 noseqinds 28082 axeuclidlem 28689 usgr2wlkneq 29482 wwlksnredwwlkn0 29619 wwlksnextwrd 29620 clwlkclwwlklem2a1 29714 lnon0 30520 hstles 31953 mdsl1i 32043 atcveq0 32070 atcvat4i 32119 cdjreui 32154 issgon 33610 connpconn 34715 outsideofrflx 35594 isbasisrelowllem1 36726 isbasisrelowllem2 36727 poimirlem3 36981 poimirlem29 37007 poimir 37011 heicant 37013 equivtotbnd 37136 ismtybndlem 37164 cvrat4 38804 linepsubN 39113 pmapsub 39129 osumcllem4N 39320 pexmidlem1N 39331 dochexmidlem1 40821 cantnfresb 42563 harval3 42778 clcnvlem 42863 iccpartimp 46570 sbgoldbwt 46930 sbgoldbst 46931 elsetrecslem 47932 |
Copyright terms: Public domain | W3C validator |