![]() |
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 254 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
3 | 2 | imp 124 | 1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 |
This theorem is referenced by: imp42 354 impr 379 anasss 399 an13s 567 3expb 1206 reuss2 3430 reupick 3434 po2nr 4327 fvmptt 5628 fliftfund 5819 f1ocnv2d 6098 addclpi 7356 addnidpig 7365 mulnqprl 7597 mulnqpru 7598 ltsubrp 9720 ltaddrp 9721 divgcdcoprm0 12133 infpnlem1 12391 imasgrp2 13052 imasrng 13310 imasring 13414 innei 14123 tgcnp 14169 isxmetd 14307 |
Copyright terms: Public domain | W3C validator |