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 4226 swopo 4278 reusv3 4432 ralxfrd 4434 rexxfrd 4435 nlimsucg 4537 poirr2 4990 elpreima 5598 fmptco 5645 tposfo2 6226 nnm00 6488 th3qlem1 6594 fiintim 6885 supmoti 6949 infglbti 6981 infnlbti 6982 updjud 7038 recexprlemss1l 7567 recexprlemss1u 7568 cauappcvgprlemladdru 7588 cauappcvgprlemladdrl 7589 caucvgprlemladdrl 7610 uzind 9293 ledivge1le 9653 xltnegi 9762 ixxssixx 9829 expnegzap 10479 shftlem 10744 cau3lem 11042 caubnd2 11045 climuni 11220 2clim 11228 summodclem2 11309 summodc 11310 zsumdc 11311 fsumf1o 11317 fisumss 11319 fsumcl2lem 11325 fsumadd 11333 fsummulc2 11375 prodmodclem2 11504 prodmodc 11505 zproddc 11506 fprodf1o 11515 fprodssdc 11517 fprodmul 11518 dfgcd2 11932 cncongrprm 12068 prmpwdvds 12264 eltg3 12604 tgidm 12621 tgrest 12716 tgcn 12755 lmtopcnp 12797 txbasval 12814 txcnp 12818 bldisj 12948 xblm 12964 blssps 12974 blss 12975 blssexps 12976 blssex 12977 metcnp3 13058 bj-findis 13702 |
Copyright terms: Public domain | W3C validator |