|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > jctl | Structured version Visualization version GIF version | ||
| Description: Inference conjoining a theorem to the left of a consequent. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 24-Oct-2012.) | 
| Ref | Expression | 
|---|---|
| jctl.1 | ⊢ 𝜓 | 
| Ref | Expression | 
|---|---|
| jctl | ⊢ (𝜑 → (𝜓 ∧ 𝜑)) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | id 22 | . 2 ⊢ (𝜑 → 𝜑) | |
| 2 | jctl.1 | . 2 ⊢ 𝜓 | |
| 3 | 1, 2 | jctil 519 | 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: mpanl1 700 mpanlr1 706 opeqsng 5507 relop 5860 odi 8618 ssfi 9214 endjudisj 10210 nn0n0n1ge2 12596 0mod 13943 expge1 14141 hashge2el2dif 14520 swrdccatin2 14768 swrd2lsw 14992 4dvdseven 16411 ndvdsp1 16449 istrkg2ld 28469 0wlkons1 30141 ococin 31428 cmbr4i 31621 iundifdif 32576 wevgblacfn 35115 nepss 35719 axextndbi 35806 ontopbas 36430 bj-elccinfty 37216 ctbssinf 37408 poimirlem16 37644 mblfinlem4 37668 ismblfin 37669 fiphp3d 42835 onmcl 43349 omabs2 43350 eelT01 44736 eel0T1 44737 un01 44814 dirkercncf 46127 nnsum3primes4 47780 vopnbgrelself 47846 line2x 48680 line2y 48681 | 
| Copyright terms: Public domain | W3C validator |