![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3impib | GIF version |
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) |
Ref | Expression |
---|---|
3impib.1 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) |
Ref | Expression |
---|---|
3impib | ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impib.1 | . . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃)) | |
2 | 1 | expd 255 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp 1140 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 927 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 929 |
This theorem is referenced by: mob 2811 eqreu 2821 funimaexglem 5131 ssimaexg 5401 dfsmo2 6090 3ecoptocl 6421 distrnq0 7115 addassnq0 7118 uzind 8956 fzind 8960 fnn0ind 8961 xltnegi 9401 facwordi 10279 shftvalg 10401 shftval4g 10402 mulgcd 11448 coprmdvds1 11516 inopn 11870 basis1 11913 xmeteq0 12161 speano5 12563 |
Copyright terms: Public domain | W3C validator |