![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3exp1 | Structured version Visualization version GIF version |
Description: Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.) |
Ref | Expression |
---|---|
3exp1.1 | ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) |
Ref | Expression |
---|---|
3exp1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp1.1 | . . 3 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃) → 𝜏) | |
2 | 1 | ex 449 | . 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → (𝜃 → 𝜏)) |
3 | 2 | 3exp 1283 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1054 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 df-an 385 df-3an 1056 |
This theorem is referenced by: 3an1rs 1312 ltmpi 9764 cshf1 13602 lcmfunsnlem 15401 mulginvcom 17612 symgfvne 17854 voliunlem3 23366 3cyclfrgrrn 27266 numclwlk1lem2foa 27344 frgrregord013 27382 strlem3a 29239 hstrlem3a 29247 chirredlem1 29377 nn0prpwlem 32442 matunitlindflem1 33535 zerdivemp1x 33876 athgt 35060 paddasslem14 35437 paddidm 35445 tendospcanN 36629 jm2.26 37886 relexpxpmin 38326 0ellimcdiv 40199 |
Copyright terms: Public domain | W3C validator |