![]() |
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 113 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | impd 251 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem is referenced by: euotd 4038 swopo 4090 reusv3 4239 ralxfrd 4241 rexxfrd 4242 nlimsucg 4338 poirr2 4768 elpreima 5340 fmptco 5384 tposfo2 5938 nnm00 6191 th3qlem1 6297 supmoti 6502 infglbti 6534 infnlbti 6535 updjud 6577 recexprlemss1l 6964 recexprlemss1u 6965 cauappcvgprlemladdru 6985 cauappcvgprlemladdrl 6986 caucvgprlemladdrl 7007 uzind 8616 ledivge1le 8961 xltnegi 9055 ixxssixx 9078 expnegzap 9684 shftlem 9930 cau3lem 10226 caubnd2 10229 climuni 10358 2clim 10366 dfgcd2 10635 cncongrprm 10768 bj-findis 11066 |
Copyright terms: Public domain | W3C validator |