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 560 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 |
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 197 df-an 386 |
This theorem is referenced by: mpanl1 716 mpanlr1 722 relop 5272 odi 7659 cdaun 8994 nn0n0n1ge2 11358 0mod 12701 expge1 12897 hashge2el2dif 13262 swrd2lsw 13695 4dvdseven 15109 ndvdsp1 15135 istrkg2ld 25359 wspthsnwspthsnon 26811 0wlkons1 26982 ococin 28267 cmbr4i 28460 iundifdif 29381 nepss 31599 axextndbi 31710 ontopbas 32427 bj-elccinfty 33101 poimirlem16 33425 mblfinlem4 33449 ismblfin 33450 fiphp3d 37383 eelT01 38936 eel0T1 38937 un01 39016 dirkercncf 40324 nnsum3primes4 41676 |
Copyright terms: Public domain | W3C validator |