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 520 | 1 ⊢ (𝜑 → (𝜓 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
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 208 df-an 397 |
This theorem is referenced by: mpanl1 696 mpanlr1 702 opeqsng 5384 relop 5714 odi 8194 endjudisj 9582 nn0n0n1ge2 11950 0mod 13258 expge1 13454 hashge2el2dif 13826 swrdccatin2 14079 swrd2lsw 14302 4dvdseven 15712 ndvdsp1 15750 istrkg2ld 26173 0wlkons1 27827 ococin 29112 cmbr4i 29305 iundifdif 30242 nepss 32845 axextndbi 32946 ontopbas 33673 bj-elccinfty 34388 ctbssinf 34569 poimirlem16 34789 mblfinlem4 34813 ismblfin 34814 fiphp3d 39294 eelT01 40922 eel0T1 40923 un01 41000 dirkercncf 42269 nnsum3primes4 43830 line2x 44669 line2y 44670 |
Copyright terms: Public domain | W3C validator |