| 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 207 df-an 396 |
| This theorem is referenced by: anc2li 555 equvini 2453 2reu1 3851 frpoinsg 6295 ordunidif 6361 isofrlem 7281 dfwe2 7714 orduniorsuc 7769 tfisg 7794 poxp 8068 fnse 8073 ssenen 9075 dffi3 9340 fpwwe2lem12 10555 zmulcl 12543 rpneg 12946 rexuz3 15275 cau3lem 15281 climrlim2 15473 o1rlimmul 15545 iseralt 15611 gcdzeq 16482 isprm3 16613 vdwnnlem2 16927 ablfaclem3 19987 epttop 22913 lmcnp 23208 dfconn2 23323 txcnp 23524 cmphaushmeo 23704 isfild 23762 cnpflf2 23904 flimfnfcls 23932 alexsubALT 23955 fgcfil 25188 bcthlem5 25245 ivthlem2 25370 ivthlem3 25371 dvfsumrlim 25955 plypf1 26134 noetalem1 27670 noseqinds 28211 axeuclidlem 28926 usgr2wlkneq 29720 wwlksnredwwlkn0 29860 wwlksnextwrd 29861 clwlkclwwlklem2a1 29955 lnon0 30761 hstles 32194 mdsl1i 32284 atcveq0 32311 atcvat4i 32360 cdjreui 32395 issgon 34109 connpconn 35227 outsideofrflx 36120 isbasisrelowllem1 37348 isbasisrelowllem2 37349 poimirlem3 37622 poimirlem29 37648 poimir 37652 heicant 37654 equivtotbnd 37777 ismtybndlem 37805 cvrat4 39442 linepsubN 39751 pmapsub 39767 osumcllem4N 39958 pexmidlem1N 39969 dochexmidlem1 41459 cantnfresb 43317 harval3 43531 clcnvlem 43616 relpfrlem 44947 iccpartimp 47421 sbgoldbwt 47781 sbgoldbst 47782 elsetrecslem 49704 |
| Copyright terms: Public domain | W3C validator |