![]() |
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 1108 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 → 𝜏)) |
4 | 3 | com12 32 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1084 |
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 206 df-an 395 df-3an 1086 |
This theorem is referenced by: 3imp2 1346 3impexp 1355 po2ne 5606 oprabidw 7450 oprabid 7451 wfrlem12OLD 8341 isinf 9285 isinfOLD 9286 infsupprpr 9529 axdc3lem4 10478 iccid 13404 difreicc 13496 relexpaddg 15036 issubg4 19108 rnglidlmcl 21124 reconn 24788 bcthlem2 25297 dvfsumrlim3 26012 ax5seg 28821 axcontlem4 28850 usgr2wlkneq 29642 frgrwopreg 30205 dfufd2lem 33361 cvmlift3lem4 35060 fscgr 35804 idinside 35808 brsegle 35832 seglecgr12im 35834 imp5q 35924 elicc3 35929 areacirclem1 37309 areacirclem2 37310 areacirclem4 37312 areacirc 37314 filbcmb 37341 fzmul 37342 islshpcv 38652 cvrat3 39042 4atexlem7 39675 relexpmulg 43279 gneispacess2 43715 iunconnlem2 44513 fmtnoprmfac1 47039 fmtnoprmfac2 47041 fpprwppr 47213 itsclc0xyqsol 48024 |
Copyright terms: Public domain | W3C validator |