![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > jctil | GIF version |
Description: Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.) |
Ref | Expression |
---|---|
jctil.1 | ⊢ (𝜑 → 𝜓) |
jctil.2 | ⊢ 𝜒 |
Ref | Expression |
---|---|
jctil | ⊢ (𝜑 → (𝜒 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jctil.2 | . . 3 ⊢ 𝜒 | |
2 | 1 | a1i 9 | . 2 ⊢ (𝜑 → 𝜒) |
3 | jctil.1 | . 2 ⊢ (𝜑 → 𝜓) | |
4 | 2, 3 | jca 300 | 1 ⊢ (𝜑 → (𝜒 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 106 |
This theorem is referenced by: jctl 307 ddifnel 3131 unidif 3685 iunxdif2 3778 exss 4054 reg2exmidlema 4350 limom 4428 xpiindim 4573 relssres 4750 funco 5054 nfunsn 5338 fliftcnv 5574 fo1stresm 5932 fo2ndresm 5933 dftpos3 6027 tfri1d 6100 rdgtfr 6139 rdgruledefgg 6140 frectfr 6165 mapxpen 6564 phplem2 6569 sbthlem2 6667 sbthlemi3 6668 djuss 6761 exmidfodomrlemr 6828 exmidfodomrlemrALT 6829 nqprrnd 7102 nqprxx 7105 ltexprlempr 7167 recexprlempr 7191 cauappcvgprlemcl 7212 caucvgprlemcl 7235 caucvgprprlemcl 7263 lemulge11 8327 nn0ge2m1nn 8733 frecfzennn 9833 demoivreALT 11063 |
Copyright terms: Public domain | W3C validator |