![]() |
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 753 3impa 1098 exp516 1123 r19.29af2 2446 mpteqb 5204 dffo3 5257 fconstfvm 5322 fliftfun 5379 tfrlem1 5864 tfrlem9 5876 nnsucsssuc 6010 nnaordex 6036 prarloclemup 6478 genpcdl 6502 genpcuu 6503 recexap 7416 zaddcllemneg 8060 zdiv 8104 uzaddcl 8305 fz0fzelfz0 8754 fz0fzdiffz0 8757 elfzmlbp 8760 difelfzle 8762 fzo1fzo0n0 8809 ssfzo12bi 8851 expivallem 8910 expcllem 8920 expap0 8939 mulexp 8948 cjexp 9121 |
Copyright terms: Public domain | W3C validator |