![]() |
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 3266 unidif 3841 iunxdif2 3935 exss 4227 reg2exmidlema 4533 limom 4613 xpiindim 4764 relssres 4945 funco 5256 nfunsn 5549 fliftcnv 5795 fo1stresm 6161 fo2ndresm 6162 dftpos3 6262 tfri1d 6335 rdgtfr 6374 rdgruledefgg 6375 frectfr 6400 elixpsn 6734 mapxpen 6847 phplem2 6852 sbthlem2 6956 sbthlemi3 6957 djuss 7068 caseinl 7089 caseinr 7090 exmidfodomrlemr 7200 exmidfodomrlemrALT 7201 2omotaplemap 7255 nqprrnd 7541 nqprxx 7544 ltexprlempr 7606 recexprlempr 7630 cauappcvgprlemcl 7651 caucvgprlemcl 7674 caucvgprprlemcl 7702 suplocsrlempr 7805 lemulge11 8822 nn0ge2m1nn 9235 frecfzennn 10425 reccn2ap 11320 demoivreALT 11780 pcdiv 12301 subrgid 13342 topcld 13579 metrest 13976 pwle2 14718 |
Copyright terms: Public domain | W3C validator |