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-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: euotd 4146 swopo 4198 reusv3 4351 ralxfrd 4353 rexxfrd 4354 nlimsucg 4451 poirr2 4901 elpreima 5507 fmptco 5554 tposfo2 6132 nnm00 6393 th3qlem1 6499 fiintim 6785 supmoti 6848 infglbti 6880 infnlbti 6881 updjud 6935 recexprlemss1l 7411 recexprlemss1u 7412 cauappcvgprlemladdru 7432 cauappcvgprlemladdrl 7433 caucvgprlemladdrl 7454 uzind 9130 ledivge1le 9481 xltnegi 9586 ixxssixx 9653 expnegzap 10295 shftlem 10556 cau3lem 10854 caubnd2 10857 climuni 11030 2clim 11038 summodclem2 11119 summodc 11120 zsumdc 11121 fsumf1o 11127 fisumss 11129 fsumcl2lem 11135 fsumadd 11143 fsummulc2 11185 dfgcd2 11629 cncongrprm 11762 eltg3 12153 tgidm 12170 tgrest 12265 tgcn 12304 lmtopcnp 12346 txbasval 12363 txcnp 12367 bldisj 12497 xblm 12513 blssps 12523 blss 12524 blssexps 12525 blssex 12526 metcnp3 12607 bj-findis 13104 |
Copyright terms: Public domain | W3C validator |