![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3impd | Structured version Visualization version GIF version |
Description: Importation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006.) |
Ref | Expression |
---|---|
3imp1.1 | ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) |
Ref | Expression |
---|---|
3impd | ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3imp1.1 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜒 → (𝜃 → 𝜏)))) | |
2 | 1 | com4l 92 | . . 3 ⊢ (𝜓 → (𝜒 → (𝜃 → (𝜑 → 𝜏)))) |
3 | 2 | 3imp 1275 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 → 𝜏)) |
4 | 3 | com12 32 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ 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: 3imp2 1304 3impexp 1311 oprabid 6717 wfrlem12 7471 isinf 8214 axdc3lem4 9313 iccid 12258 difreicc 12342 relexpaddg 13837 issubg4 17660 reconn 22678 bcthlem2 23168 dvfsumrlim3 23841 ax5seg 25863 axcontlem4 25892 usgr2wlkneq 26708 frgrwopreg 27303 cvmlift3lem4 31430 fscgr 32312 idinside 32316 brsegle 32340 seglecgr12im 32342 imp5q 32431 elicc3 32436 areacirclem1 33630 areacirclem2 33631 areacirclem4 33633 areacirc 33635 filbcmb 33665 fzmul 33667 islshpcv 34658 cvrat3 35046 4atexlem7 35679 relexpmulg 38319 gneispacess2 38761 iunconnlem2 39485 fmtnoprmfac1 41802 fmtnoprmfac2 41804 |
Copyright terms: Public domain | W3C validator |