![]() |
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 115 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | impd 254 | 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-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem is referenced by: euotd 4272 swopo 4324 reusv3 4478 ralxfrd 4480 rexxfrd 4481 nlimsucg 4583 poirr2 5039 elpreima 5656 fmptco 5703 tposfo2 6292 nnm00 6555 th3qlem1 6663 fiintim 6957 supmoti 7022 infglbti 7054 infnlbti 7055 updjud 7111 recexprlemss1l 7664 recexprlemss1u 7665 cauappcvgprlemladdru 7685 cauappcvgprlemladdrl 7686 caucvgprlemladdrl 7707 uzind 9394 ledivge1le 9756 xltnegi 9865 ixxssixx 9932 expnegzap 10585 shftlem 10857 cau3lem 11155 caubnd2 11158 climuni 11333 2clim 11341 summodclem2 11422 summodc 11423 zsumdc 11424 fsumf1o 11430 fisumss 11432 fsumcl2lem 11438 fsumadd 11446 fsummulc2 11488 prodmodclem2 11617 prodmodc 11618 zproddc 11619 fprodf1o 11628 fprodssdc 11630 fprodmul 11631 dfgcd2 12047 cncongrprm 12189 prmpwdvds 12387 infpnlem1 12391 1arith 12399 isgrpid2 12984 dvdsrd 13444 dvdsrtr 13451 dvdsrmul1 13452 unitgrp 13466 eltg3 14017 tgidm 14034 tgrest 14129 tgcn 14168 lmtopcnp 14210 txbasval 14227 txcnp 14231 bldisj 14361 xblm 14377 blssps 14387 blss 14388 blssexps 14389 blssex 14390 metcnp3 14471 2sqlem6 14928 2sqlem7 14929 bj-findis 15192 |
Copyright terms: Public domain | W3C validator |