![]() |
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 518 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 395 |
This theorem is referenced by: mpanl1 698 mpanlr1 704 opeqsng 5501 relop 5849 odi 8601 ssfi 9204 endjudisj 10204 nn0n0n1ge2 12585 0mod 13916 expge1 14113 hashge2el2dif 14494 swrdccatin2 14732 swrd2lsw 14956 4dvdseven 16370 ndvdsp1 16408 istrkg2ld 28384 0wlkons1 30051 ococin 31338 cmbr4i 31531 iundifdif 32483 wevgblacfn 34949 nepss 35553 axextndbi 35641 ontopbas 36153 bj-elccinfty 36934 ctbssinf 37126 poimirlem16 37350 mblfinlem4 37374 ismblfin 37375 fiphp3d 42513 onmcl 43034 omabs2 43035 eelT01 44424 eel0T1 44425 un01 44502 dirkercncf 45764 nnsum3primes4 47396 vopnbgrelself 47458 line2x 48178 line2y 48179 |
Copyright terms: Public domain | W3C validator |