![]() |
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 258 | . 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃))) |
3 | 2 | 3imp 1195 | 1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∧ w3a 980 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: mob 2934 eqreu 2944 iotam 5224 funimaexglem 5315 ssimaexg 5595 rbropap 6263 dfsmo2 6307 3ecoptocl 6645 distrnq0 7483 addassnq0 7486 uzind 9389 fzind 9393 fnn0ind 9394 xltnegi 9860 facwordi 10747 shftvalg 10872 shftval4g 10873 mulgcd 12044 coprmdvds1 12118 pcfac 12377 mgmcl 12828 mhmlin 12912 mhmmulg 13096 issubg2m 13121 nsgbi 13136 srgmulgass 13336 dvdsrtr 13444 issubrng2 13550 issubrg2 13581 inopn 13940 basis1 13984 cnmpt2t 14230 cnmpt22 14231 cnmptcom 14235 xmeteq0 14296 sincosq1sgn 14684 sincosq2sgn 14685 sincosq3sgn 14686 sincosq4sgn 14687 speano5 15134 |
Copyright terms: Public domain | W3C validator |