![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3expd | Structured version Visualization version GIF version |
Description: Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.) |
Ref | Expression |
---|---|
3expd.1 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
Ref | Expression |
---|---|
3expd | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3expd.1 | . . . 4 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) | |
2 | 1 | com12 32 | . . 3 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 → 𝜏)) |
3 | 2 | 3exp 1256 | . 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏)))) |
4 | 3 | com4r 92 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1031 |
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 196 df-an 385 df-3an 1033 |
This theorem is referenced by: 3exp2 1277 exp516 1279 3impexp 1281 smogt 7351 axdc3lem4 9158 axcclem 9162 caubnd 13946 coprmprod 15213 catidd 16164 mulgnnass 17399 mulgnnassOLD 17400 mclsind 30721 fscgr 31357 cvrat4 33747 3dim1 33771 3dim2 33772 llnle 33822 lplnle 33844 llncvrlpln2 33861 lplncvrlvol2 33919 pmaple 34065 paddasslem14 34137 paddasslem15 34138 osumcllem11N 34270 cdlemeg46gfre 34838 cdlemk33N 35215 dia2dimlem6 35376 lclkrlem2y 35838 relexpmulnn 37020 3impexpbicom 37706 icceuelpart 39974 |
Copyright terms: Public domain | W3C validator |