![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > expimpd | GIF version |
Description: Exportation followed by a deduction version of importation. (Contributed by NM, 6-Sep-2008.) |
Ref | Expression |
---|---|
expimpd.1 | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
Ref | Expression |
---|---|
expimpd | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | expimpd.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) | |
2 | 1 | ex 114 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | impd 252 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: euotd 4136 swopo 4188 reusv3 4341 ralxfrd 4343 rexxfrd 4344 nlimsucg 4441 poirr2 4889 elpreima 5493 fmptco 5540 tposfo2 6118 nnm00 6379 th3qlem1 6485 fiintim 6770 supmoti 6832 infglbti 6864 infnlbti 6865 updjud 6919 recexprlemss1l 7391 recexprlemss1u 7392 cauappcvgprlemladdru 7412 cauappcvgprlemladdrl 7413 caucvgprlemladdrl 7434 uzind 9066 ledivge1le 9412 xltnegi 9511 ixxssixx 9578 expnegzap 10220 shftlem 10481 cau3lem 10778 caubnd2 10781 climuni 10954 2clim 10962 summodclem2 11043 summodc 11044 zsumdc 11045 fsumf1o 11051 fisumss 11053 fsumcl2lem 11059 fsumadd 11067 fsummulc2 11109 dfgcd2 11548 cncongrprm 11681 eltg3 12069 tgidm 12086 tgrest 12181 tgcn 12219 lmtopcnp 12261 txbasval 12278 txcnp 12282 bldisj 12390 xblm 12406 blssps 12416 blss 12417 blssexps 12418 blssex 12419 metcnp3 12500 bj-findis 12869 |
Copyright terms: Public domain | W3C validator |