![]() |
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 512 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 |
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 199 df-an 388 |
This theorem is referenced by: mpanl1 688 mpanlr1 694 opeqsng 5245 relop 5567 odi 8004 endjudisj 9390 nn0n0n1ge2 11772 0mod 13083 expge1 13279 hashge2el2dif 13647 swrd2lsw 14174 4dvdseven 15582 ndvdsp1 15620 istrkg2ld 25963 clwlkclwwlkfOLD 27533 0wlkons1 27665 ococin 28981 cmbr4i 29174 iundifdif 30100 nepss 32505 axextndbi 32607 ontopbas 33333 bj-elccinfty 34002 ctbssinf 34165 poimirlem16 34386 mblfinlem4 34410 ismblfin 34411 fiphp3d 38850 eelT01 40501 eel0T1 40502 un01 40579 dirkercncf 41855 nnsum3primes4 43353 line2x 44141 line2y 44142 |
Copyright terms: Public domain | W3C validator |