| 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 1120 | . 2 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏)))) |
| 4 | 3 | com4r 94 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ w3a 1087 |
| 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 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: 3exp2 1355 exp516 1357 3impexp 1359 smogt 8407 axdc3lem4 10493 axcclem 10497 caubnd 15397 coprmprod 16698 catidd 17723 mulgnnass 19127 numedglnl 29161 mclsind 35575 fscgr 36081 cvrat4 39445 3dim1 39469 3dim2 39470 llnle 39520 lplnle 39542 llncvrlpln2 39559 lplncvrlvol2 39617 pmaple 39763 paddasslem14 39835 paddasslem15 39836 osumcllem11N 39968 cdlemeg46gfre 40534 cdlemk33N 40911 dia2dimlem6 41071 lclkrlem2y 41533 rexlimdv3d 42694 relexpmulnn 43722 3impexpbicom 44500 icceuelpart 47423 grlimgrtri 47963 |
| Copyright terms: Public domain | W3C validator |