Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > imp32 | GIF version |
Description: An importation inference. (Contributed by NM, 26-Apr-1994.) |
Ref | Expression |
---|---|
imp3.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
Ref | Expression |
---|---|
imp32 | ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imp3.1 | . . 3 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) | |
2 | 1 | impd 252 | . 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 |
This theorem is referenced by: imp42 351 impr 376 anasss 396 an13s 556 3expb 1182 reuss2 3356 reupick 3360 po2nr 4231 fvmptt 5512 fliftfund 5698 f1ocnv2d 5974 addclpi 7135 addnidpig 7144 mulnqprl 7376 mulnqpru 7377 ltsubrp 9478 ltaddrp 9479 divgcdcoprm0 11782 innei 12332 tgcnp 12378 isxmetd 12516 |
Copyright terms: Public domain | W3C validator |