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 256 | . 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-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem is referenced by: rexlimdvv 2554 reu6 2868 fun11iun 5381 poxp 6122 smoel 6190 iinerm 6494 suplub2ti 6881 infglbti 6905 infnlbti 6906 prarloclemlo 7295 peano5uzti 9152 lbzbi 9401 ssfzo12bi 9995 cau3lem 10879 summodc 11145 mertenslem2 11298 alzdvds 11541 nno 11592 nn0seqcvgd 11711 lcmdvds 11749 divgcdodd 11810 cnptoprest 12397 lmss 12404 txlm 12437 |
Copyright terms: Public domain | W3C validator |