![]() |
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 4209 swopo 4261 reusv3 4414 ralxfrd 4416 rexxfrd 4417 nlimsucg 4519 poirr2 4971 elpreima 5579 fmptco 5626 tposfo2 6204 nnm00 6465 th3qlem1 6571 fiintim 6862 supmoti 6925 infglbti 6957 infnlbti 6958 updjud 7012 recexprlemss1l 7534 recexprlemss1u 7535 cauappcvgprlemladdru 7555 cauappcvgprlemladdrl 7556 caucvgprlemladdrl 7577 uzind 9254 ledivge1le 9611 xltnegi 9717 ixxssixx 9784 expnegzap 10431 shftlem 10693 cau3lem 10991 caubnd2 10994 climuni 11167 2clim 11175 summodclem2 11256 summodc 11257 zsumdc 11258 fsumf1o 11264 fisumss 11266 fsumcl2lem 11272 fsumadd 11280 fsummulc2 11322 prodmodclem2 11451 prodmodc 11452 zproddc 11453 fprodf1o 11462 fprodssdc 11464 fprodmul 11465 dfgcd2 11869 cncongrprm 12002 eltg3 12396 tgidm 12413 tgrest 12508 tgcn 12547 lmtopcnp 12589 txbasval 12606 txcnp 12610 bldisj 12740 xblm 12756 blssps 12766 blss 12767 blssexps 12768 blssex 12769 metcnp3 12850 bj-findis 13492 |
Copyright terms: Public domain | W3C validator |