![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > expdimp | GIF version |
Description: A deduction version of exportation, followed by importation. (Contributed by NM, 6-Sep-2008.) |
Ref | Expression |
---|---|
exp3a.1 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Ref | Expression |
---|---|
expdimp | ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp3a.1 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | |
2 | 1 | expd 255 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | imp 123 | 1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: rexlimdvv 2496 reu6 2805 fun11iun 5287 poxp 6011 smoel 6079 iinerm 6378 suplub2ti 6750 infglbti 6774 infnlbti 6775 prarloclemlo 7114 peano5uzti 8915 lbzbi 9162 ssfzo12bi 9697 cau3lem 10608 isummo 10834 mertenslem2 10991 alzdvds 11194 nno 11245 nn0seqcvgd 11362 lcmdvds 11400 divgcdodd 11461 |
Copyright terms: Public domain | W3C validator |