![]() |
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 1104 | . 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜃) → (𝜑 → 𝜏)) |
4 | 3 | com12 32 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒 ∧ 𝜃) → 𝜏)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ w3a 1080 |
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 208 df-an 397 df-3an 1082 |
This theorem is referenced by: 3imp2 1342 3impexp 1351 po2ne 5377 oprabid 7047 wfrlem12 7818 isinf 8577 infsupprpr 8814 axdc3lem4 9721 iccid 12633 difreicc 12720 relexpaddg 14246 issubg4 18052 reconn 23119 bcthlem2 23611 dvfsumrlim3 24313 ax5seg 26407 axcontlem4 26436 usgr2wlkneq 27224 frgrwopreg 27794 cvmlift3lem4 32177 fscgr 33150 idinside 33154 brsegle 33178 seglecgr12im 33180 imp5q 33269 elicc3 33274 areacirclem1 34513 areacirclem2 34514 areacirclem4 34516 areacirc 34518 filbcmb 34547 fzmul 34548 islshpcv 35720 cvrat3 36109 4atexlem7 36742 relexpmulg 39540 gneispacess2 39981 iunconnlem2 40808 fmtnoprmfac1 43209 fmtnoprmfac2 43211 fpprwppr 43386 itsclc0xyqsol 44236 |
Copyright terms: Public domain | W3C validator |