![]() |
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 306 | 1 ⊢ (𝜑 → (𝜒 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 |
This theorem is referenced by: jctl 314 ddifnel 3278 unidif 3853 iunxdif2 3947 exss 4239 reg2exmidlema 4545 limom 4625 xpiindim 4776 relssres 4957 funco 5268 nfunsn 5561 fliftcnv 5809 fo1stresm 6175 fo2ndresm 6176 dftpos3 6276 tfri1d 6349 rdgtfr 6388 rdgruledefgg 6389 frectfr 6414 elixpsn 6748 mapxpen 6861 phplem2 6866 sbthlem2 6970 sbthlemi3 6971 djuss 7082 caseinl 7103 caseinr 7104 exmidfodomrlemr 7214 exmidfodomrlemrALT 7215 2omotaplemap 7269 nqprrnd 7555 nqprxx 7558 ltexprlempr 7620 recexprlempr 7644 cauappcvgprlemcl 7665 caucvgprlemcl 7688 caucvgprprlemcl 7716 suplocsrlempr 7819 lemulge11 8836 nn0ge2m1nn 9249 frecfzennn 10439 reccn2ap 11334 demoivreALT 11794 pcdiv 12315 subrgid 13438 topcld 13880 metrest 14277 pwle2 15020 |
Copyright terms: Public domain | W3C validator |