![]() |
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 113 | . 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃)) |
3 | 2 | ex 113 | 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-ia3 106 |
This theorem is referenced by: exp41 362 exp42 363 expl 370 exbiri 374 anasss 391 an31s 535 con4biddc 788 3impa 1134 exp516 1159 r19.29af2 2502 mpteqb 5315 dffo3 5368 fconstfvm 5433 fliftfun 5489 tfrlem1 5979 tfrlem9 5990 tfr1onlemaccex 6019 tfrcllemaccex 6032 tfrcl 6035 nnsucsssuc 6158 nnaordex 6189 diffifi 6452 prarloclemup 6824 genpcdl 6848 genpcuu 6849 negf1o 7630 recexap 7887 zaddcllemneg 8548 zdiv 8593 uzaddcl 8832 fz0fzelfz0 9292 fz0fzdiffz0 9295 elfzmlbp 9297 difelfzle 9299 fzo1fzo0n0 9346 ssfzo12bi 9388 exfzdc 9403 modfzo0difsn 9554 frecuzrdgg 9575 iseqvalt 9609 expivallem 9651 expcllem 9661 expap0 9680 mulexp 9689 cjexp 10006 absexp 10191 fimaxre2 10335 divconjdvds 10482 addmodlteqALT 10492 divalglemeunn 10553 divalglemeuneg 10555 zsupcllemstep 10573 bezoutlemstep 10618 bezoutlemmain 10619 dfgcd2 10635 pw2dvdslemn 10775 |
Copyright terms: Public domain | W3C validator |