![]() |
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 559 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 385 |
This theorem is referenced by: mpanl1 716 mpanlr1 722 relop 5305 odi 7704 cdaun 9032 nn0n0n1ge2 11396 0mod 12741 expge1 12937 hashge2el2dif 13300 swrd2lsw 13741 4dvdseven 15156 ndvdsp1 15182 istrkg2ld 25404 wspthsnwspthsnonOLD 26881 0wlkons1 27099 ococin 28395 cmbr4i 28588 iundifdif 29507 nepss 31725 axextndbi 31834 ontopbas 32552 bj-elccinfty 33231 poimirlem16 33555 mblfinlem4 33579 ismblfin 33580 fiphp3d 37700 eelT01 39253 eel0T1 39254 un01 39333 dirkercncf 40642 nnsum3primes4 42001 |
Copyright terms: Public domain | W3C validator |