![]() |
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 242 | . 2 ⊢ (φ → ((ψ ∧ χ) → θ)) |
3 | 2 | imp 115 | 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-ia1 99 ax-ia2 100 |
This theorem is referenced by: imp42 336 impr 361 anasss 379 an13s 501 3expb 1104 reuss2 3211 reupick 3215 po2nr 4037 fvmptt 5205 fliftfund 5380 f1ocnv2d 5646 addclpi 6311 addnidpig 6320 mulnqprl 6549 mulnqpru 6550 ltsubrp 8392 ltaddrp 8393 |
Copyright terms: Public domain | W3C validator |