Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > exp31 | GIF version |
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
exp31.1 | ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) |
Ref | Expression |
---|---|
exp31 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exp31.1 | . . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃) | |
2 | 1 | ex 108 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
3 | 2 | ex 108 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia3 101 |
This theorem is referenced by: exp41 352 exp42 353 expl 360 exbiri 364 anasss 379 an31s 504 con4biddc 754 3impa 1099 exp516 1124 r19.29af2 2452 mpteqb 5261 dffo3 5314 fconstfvm 5379 fliftfun 5436 tfrlem1 5923 tfrlem9 5935 nnsucsssuc 6071 nnaordex 6100 diffifi 6351 prarloclemup 6593 genpcdl 6617 genpcuu 6618 recexap 7634 zaddcllemneg 8284 zdiv 8328 uzaddcl 8529 fz0fzelfz0 8984 fz0fzdiffz0 8987 elfzmlbp 8990 difelfzle 8992 fzo1fzo0n0 9039 ssfzo12bi 9081 expivallem 9256 expcllem 9266 expap0 9285 mulexp 9294 cjexp 9493 absexp 9675 |
Copyright terms: Public domain | W3C validator |