![]() |
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 521 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 |
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 398 |
This theorem is referenced by: mpanl1 699 mpanlr1 705 opeqsng 5465 relop 5811 odi 8531 ssfi 9124 endjudisj 10111 nn0n0n1ge2 12487 0mod 13814 expge1 14012 hashge2el2dif 14386 swrdccatin2 14624 swrd2lsw 14848 4dvdseven 16262 ndvdsp1 16300 istrkg2ld 27444 0wlkons1 29107 ococin 30392 cmbr4i 30585 iundifdif 31523 nepss 34329 axextndbi 34418 ontopbas 34929 bj-elccinfty 35714 ctbssinf 35906 poimirlem16 36123 mblfinlem4 36147 ismblfin 36148 fiphp3d 41171 onmcl 41695 omabs2 41696 eelT01 43067 eel0T1 43068 un01 43145 dirkercncf 44422 nnsum3primes4 46054 line2x 46914 line2y 46915 |
Copyright terms: Public domain | W3C validator |